vampire-sys 0.5.2

Low-level FFI bindings to the Vampire theorem prover (use the 'vampire' crate instead)
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79

/*
 * This file is part of the source code of the software program
 * Vampire. It is protected by applicable
 * copyright laws.
 *
 * This source code is distributed under the licence found here
 * https://vprover.github.io/license.html
 * and in the source directory
 */
/**
 * @file Z3MainLoop.cpp
 * Defines class Z3MainLoop.
 */

#if VZ3

#include "Forwards.hpp"
#include "Kernel/Clause.hpp"

#include "Z3Interfacing.hpp"

#include "Z3MainLoop.hpp"

namespace SAT
{

using namespace Shell;
using namespace Lib;

Z3MainLoop::Z3MainLoop(Problem& prb, const Options& opt)
: MainLoop(prb,opt)
{
}

void Z3MainLoop::init()
{
}

MainLoopResult Z3MainLoop::runImpl()
{
  if(!_prb.getProperty()->allNonTheoryClausesGround()){
    return MainLoopResult(TerminationReason::INAPPROPRIATE);
  }

  SAT2FO s2f;
  Z3Interfacing solver(_opt,s2f, /* unsat core */ false, /* export smtlib problem */ "", Options::ProblemExportSyntax::SMTLIB);

 ClauseIterator cit(_prb.clauseIterator());
 while(cit.hasNext()){
   Clause* cl = cit.next();

   if(cl->varCnt() > 0){
     ASS(cl->isTheoryAxiom());
     continue;
   }

   unsigned len = cl->size();
   SATClause* sc = new(len) SATClause(len);
   unsigned i=0;
   for (auto l : cl->iterLits()) {
     SATLiteral sl = s2f.toSAT(l);
     (*sc)[i++] = sl;
   }
   solver.addClause(sc);
 }

 Status status = solver.solveLimited(UINT_MAX);

 TerminationReason reason = TerminationReason::UNKNOWN;

 if(status == Status::UNSATISFIABLE){ reason = TerminationReason::REFUTATION; }
 if(status == Status::SATISFIABLE){ reason = TerminationReason::SATISFIABLE; }

 return MainLoopResult(reason);
}

}

#endif