SATSolver *newS;
if (bm->UserFlags.solver_to_use == UserDefinedFlags::SIMPLIFYING_MINISAT_SOLVER)
- newS = new SimplifyingMinisat();
+ newS = new SimplifyingMinisat(bm->soft_timeout_expired);
else if (bm->UserFlags.solver_to_use == UserDefinedFlags::CRYPTOMINISAT_SOLVER)
newS = new CryptoMinisat();
else if (bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_SOLVER)
- newS = new MinisatCore<Minisat::Solver>();
+ newS = new MinisatCore<Minisat::Solver>(bm->soft_timeout_expired);
else if (bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_PROPAGATORS)
- newS = new MinisatCore_prop<Minisat::Solver_prop>();
+ newS = new MinisatCore_prop<Minisat::Solver_prop>(bm->soft_timeout_expired);
cerr << "Difficulty Initially:" << difficulty.score(original_input) << endl;
// A heap object so I can easily control its lifetime.
- BVSolver* bvSolver = new BVSolver(bm, simp);
- PropagateEqualities * pe = new PropagateEqualities(simp,bm->defaultNodeFactory,bm);
+ std::auto_ptr<BVSolver> bvSolver(new BVSolver(bm, simp));
+ std::auto_ptr<PropagateEqualities> pe (new PropagateEqualities(simp,bm->defaultNodeFactory,bm));
ASTNode simplified_solved_InputToSAT = original_input;
assert(!arrayops);
// Run size reducing just once.
- simplified_solved_InputToSAT = sizeReducing(simplified_solved_InputToSAT, bvSolver,pe);
+ simplified_solved_InputToSAT = sizeReducing(simplified_solved_InputToSAT, bvSolver.get(),pe.get());
unsigned initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT);
// Currently we discards all the state each time sizeReducing is called,
// so it's expensive to call.
if ((!arrayops && initial_difficulty_score < 1000000) || bm->UserFlags.isSet("preserving-fixedpoint", "0"))
- simplified_solved_InputToSAT = callSizeReducing(simplified_solved_InputToSAT, bvSolver,pe, initial_difficulty_score);
+ simplified_solved_InputToSAT = callSizeReducing(simplified_solved_InputToSAT, bvSolver.get(),pe.get(), initial_difficulty_score);
if ((!arrayops || bm->UserFlags.isSet("array-difficulty-reversion", "1")))
{
cout << "Difficulty After Size reducing:" << initial_difficulty_score << endl;
// So we can delete the object and release all the hash-buckets storage.
- Revert_to* revert = new Revert_to();
+ auto_ptr<Revert_to> revert(new Revert_to());
if ((!arrayops || bm->UserFlags.isSet("array-difficulty-reversion", "1")))
{
{
inputToSAT = simplified_solved_InputToSAT;
+ if (bm->soft_timeout_expired)
+ return SOLVER_TIMEOUT;
+
if (bm->UserFlags.optimize_flag)
{
simplified_solved_InputToSAT = pe->topLevel(simplified_solved_InputToSAT, arrayTransformer);
}
}
+ if (bm->soft_timeout_expired)
+ return SOLVER_TIMEOUT;
+
// Simplify using Ite context
if (bm->UserFlags.optimize_flag && bm->UserFlags.isSet("ite-context", "0"))
{
// it to put back in all the bad simplifications.
bm->UserFlags.optimize_flag = false;
}
- delete revert;
+ revert.reset(NULL);
simplified_solved_InputToSAT = arrayTransformer->TransformFormula_TopLevel(simplified_solved_InputToSAT);
bm->ASTNodeStats("after transformation: ", simplified_solved_InputToSAT);
bm->ClearAllTables();
// Deleting it clears out all the buckets associated with hashmaps etc. too.
- delete bvSolver;
- bvSolver = NULL;
- delete pe;
- pe = NULL;
+ bvSolver.reset(NULL);
+ pe.reset(NULL);
+
if (bm->UserFlags.stats_flag)
simp->printCacheStatus();
ToSATBase* satBase = bm->UserFlags.isSet("traditional-cnf", "0") ? tosat : ((ToSAT*) &toSATAIG) ;
+ if (bm->soft_timeout_expired)
+ return SOLVER_TIMEOUT;
+
// If it doesn't contain array operations, use ABC's CNF generation.
res = Ctr_Example->CallSAT_ResultCheck(NewSolver, simplified_solved_InputToSAT, original_input, satBase,
maybeRefinement);
+ if (bm->soft_timeout_expired)
+ {
+ if (toSATAIG.cbIsDestructed())
+ cleaner.release();
+
+ return SOLVER_TIMEOUT;
+ }
if (SOLVER_UNDECIDED != res)
{
// If the aig converter knows that it is never going to be called again,
uint8_t last_iteration;
- public:
+ public:
HashingNodeFactory* hashingNodeFactory;
NodeFactory *defaultNodeFactory;
//frequently used nodes
ASTNode ASTFalse, ASTTrue, ASTUndefined;
+ volatile bool soft_timeout_expired;
+
// No nodes should already have the iteration number that is returned from here.
// This never returns zero.
uint8_t getNextIteration()
UserFlags(),
_symbol_count(0),
CNFFileNameCounter(0),
- last_iteration(0)
+ last_iteration(0),
+ soft_timeout_expired(false)
{
_max_node_num = 0;
bool sat = tosat->CallSAT(SatSolver, modified_input, refinement);
+ if (bm->soft_timeout_expired)
+ return SOLVER_TIMEOUT;
+
if (!sat)
{
//PrintOutput(true);
b->AddAssert(*a, absrefine_bucket_num);
}
+void soft_time_out(int ignored)
+{
+ BEEV::ParserBM->soft_timeout_expired = true;
+}
//! Check validity of e in the current context. e must be a FORMULA
//
* the starting context. If the result is false, then the resulting
* context is a context in which e is false. e must have Boolean
* type. */
-int vc_query(VC vc, Expr e) {
+int vc_query(VC vc, Expr e, int timeout_ms) {
nodestar a = (nodestar)e;
stpstar stp = ((stpstar)vc);
bmstar b = (bmstar)(stp->bm);
+ assert(!BEEV::ParserBM->soft_timeout_expired);
+ if (timeout_ms != -1)
+ {
+ itimerval timeout;
+ signal(SIGVTALRM, soft_time_out);
+ timeout.it_interval.tv_usec = 0;
+ timeout.it_interval.tv_sec = 0;
+ timeout.it_value.tv_usec = 1000 * (timeout_ms % 1000);
+ timeout.it_value.tv_sec = timeout_ms / 1000;
+ setitimer(ITIMER_VIRTUAL, &timeout, NULL);
+ }
+
if(!BEEV::is_Form_kind(a->GetKind()))
{
BEEV::FatalError("CInterface: Trying to QUERY a NON formula: ",*a);
{
output = stp->TopLevelSTP(b->CreateNode(BEEV::TRUE),*a);
}
+
+ if (timeout_ms !=-1)
+ {
+ // Reset the timer.
+ setitimer(ITIMER_VIRTUAL, NULL, NULL);
+ BEEV::ParserBM->soft_timeout_expired = false;
+ }
+
return output;
} //end of vc_query
BEEV::ASTNode asserts = (*(BEEV::ASTVec*)AssertsQuery)[0];
BEEV::ASTNode query = (*(BEEV::ASTVec*)AssertsQuery)[1];
- //BEEV::GlobalSTP->TopLevelSTP(asserts, query);
+
node oo = b->CreateNode(BEEV::NOT,query);
node o = b->CreateNode(BEEV::AND,asserts,oo);
//if returned 1 then input is VALID
//
//if returned 2 then ERROR
- int vc_query(VC vc, Expr e);
+
+ // NB. The timeout is a soft timeout, use the -g flag for a hard timeout that
+ // will abort automatically. The soft timeout is checked sometimes in the code,
+ // and if the time has passed, then "timeout" will be returned. It's only checked
+ // sometimes though, so the actual timeout may be larger. Cryptominisat doesn't check
+ // the timeout yet..
+ int vc_query(VC vc, Expr e, int timeout_ms= -1);
+
//! Return the counterexample after a failed query.
Expr vc_getCounterExample(VC vc, Expr e);
{
SOLVER_INVALID=0,
SOLVER_VALID=1,
- SOLVER_UNDECIDED=2,
+ SOLVER_UNDECIDED=2,
+ SOLVER_TIMEOUT=3,
SOLVER_ERROR=-100,
SOLVER_UNSATISFIABLE = 1,
SOLVER_SATISFIABLE = 0
{
template <class T>
- MinisatCore<T>::MinisatCore()
+ MinisatCore<T>::MinisatCore(volatile bool& interrupt)
{
- s = new T();
+ s = new T(interrupt);
};
template <class T>
T * s;
public:
- MinisatCore();
+ MinisatCore(volatile bool& interrupt);
~MinisatCore();
{
template <class T>
- MinisatCore_prop<T>::MinisatCore_prop()
+ MinisatCore_prop<T>::MinisatCore_prop(volatile bool& timeout)
{
- s = new T();
+ s = new T(timeout);
};
template <class T>
T * s;
public:
- MinisatCore_prop();
+ MinisatCore_prop(volatile bool& timeout);
~MinisatCore_prop();
namespace BEEV
{
- SimplifyingMinisat::SimplifyingMinisat()
+ SimplifyingMinisat::SimplifyingMinisat(volatile bool& timeout)
{
- s = new Minisat::SimpSolver();
+ s = new Minisat::SimpSolver(timeout);
}
SimplifyingMinisat::~SimplifyingMinisat()
public:
- SimplifyingMinisat();
+ SimplifyingMinisat(volatile bool& timeout);
~SimplifyingMinisat();
bool
// Constructor/Destructor:
-Solver::Solver() :
+Solver::Solver(volatile bool& interrupt) :
// Parameters (user settable):
//
//
, conflict_budget (-1)
, propagation_budget (-1)
- , asynch_interrupt (false)
+ , asynch_interrupt (interrupt)
{}
// Constructor/Destructor:
//
- Solver();
+ Solver(volatile bool& interrupt);
virtual ~Solver();
// Problem specification:
//
int64_t conflict_budget; // -1 means no budget.
int64_t propagation_budget; // -1 means no budget.
- bool asynch_interrupt;
+ volatile bool& asynch_interrupt;
// Main internal methods:
//
//=================================================================================================
// Constructor/Destructor:
-Solver_prop::Solver_prop() :
+Solver_prop::Solver_prop(volatile bool& timeout) :
// Parameters (user settable):
//
//
, conflict_budget (-1)
, propagation_budget (-1)
- , asynch_interrupt (false)
+ , asynch_interrupt (timeout)
{}
public:
// Constructor/Destructor:
//
- Solver_prop();
+ Solver_prop(volatile bool& timeout);
virtual ~Solver_prop();
// Problem specification:
//
int64_t conflict_budget; // -1 means no budget.
int64_t propagation_budget; // -1 means no budget.
- bool asynch_interrupt;
+ volatile bool& asynch_interrupt;
// Main internal methods:
//
// Constructor/Destructor:
-SimpSolver::SimpSolver() :
+SimpSolver::SimpSolver(volatile bool& interrupt) :
+ Solver(interrupt),
grow (opt_grow)
, clause_lim (opt_clause_lim)
, subsumption_lim (opt_subsumption_lim)
public:
// Constructor/Destructor:
//
- SimpSolver();
+ SimpSolver(volatile bool& interrupt);
~SimpSolver();
// Problem specification:
g++ $(CXXFLAGS) push-no-pop.c -o a28.out $(LIBS)
$(VALGRIND) ./a28.out
+29:
+ g++ $(CXXFLAGS) timeout.c -o a29.out $(LIBS)
+ ./a29.out
+
clean:
rm -rf *~ *.out *.dSYM
--- /dev/null
+(benchmark icbrtorinvalidvc.smt
+:source {
+Integer cube root algorithm icbrt(x), where x is an unsigned 32 bit integer.
+From the book "Hacker's delight" by Henry S. Warren, Jr., page 212
+We use "or" instead of "add" to increment values inside the loop.
+
+We try to show the invalid verification condition:
+y^3 == x or (y^3 < x and (y+1)^3 > x) holds, where y is the result.
+
+Contributed by Robert Brummayer (robert.brummayer@gmail.com)
+}
+:status sat
+:category { crafted }
+:logic QF_BV
+:extrafuns ((x BitVec[32]))
+:formula
+(let (?e2 bv30[5])
+(let (?e3 bv0[32])
+(let (?e4 bv1[32])
+(let (?e5 bv2[32])
+(let (?e6 bv3[32])
+(let (?e7 bv3[5])
+(let (?e8 (bvmul ?e3 ?e5))
+(let (?e9 (bvor ?e8 ?e4))
+(let (?e10 (bvmul ?e8 ?e6))
+(let (?e11 (bvmul ?e10 ?e9))
+(let (?e12 (bvor ?e11 ?e4))
+(let (?e13 (bvshl ?e12 (zero_extend[27] ?e2)))
+(let (?e14 (bvsub ?e2 ?e7))
+(let (?e15 (ite (bvuge x ?e13) bv1[1] bv0[1]))
+(let (?e16 (bvsub x ?e13))
+(let (?e17 (ite (= bv1[1] ?e15) ?e16 x))
+(let (?e18 (bvor ?e8 ?e4))
+(let (?e19 (ite (= bv1[1] ?e15) ?e18 ?e8))
+(let (?e20 (bvmul ?e19 ?e5))
+(let (?e21 (bvor ?e20 ?e4))
+(let (?e22 (bvmul ?e20 ?e6))
+(let (?e23 (bvmul ?e22 ?e21))
+(let (?e24 (bvor ?e23 ?e4))
+(let (?e25 (bvshl ?e24 (zero_extend[27] ?e14)))
+(let (?e26 (bvsub ?e14 ?e7))
+(let (?e27 (ite (bvuge ?e17 ?e25) bv1[1] bv0[1]))
+(let (?e28 (bvsub ?e17 ?e25))
+(let (?e29 (ite (= bv1[1] ?e27) ?e28 ?e17))
+(let (?e30 (bvor ?e20 ?e4))
+(let (?e31 (ite (= bv1[1] ?e27) ?e30 ?e20))
+(let (?e32 (bvmul ?e31 ?e5))
+(let (?e33 (bvor ?e32 ?e4))
+(let (?e34 (bvmul ?e32 ?e6))
+(let (?e35 (bvmul ?e34 ?e33))
+(let (?e36 (bvor ?e35 ?e4))
+(let (?e37 (bvshl ?e36 (zero_extend[27] ?e26)))
+(let (?e38 (bvsub ?e26 ?e7))
+(let (?e39 (ite (bvuge ?e29 ?e37) bv1[1] bv0[1]))
+(let (?e40 (bvsub ?e29 ?e37))
+(let (?e41 (ite (= bv1[1] ?e39) ?e40 ?e29))
+(let (?e42 (bvor ?e32 ?e4))
+(let (?e43 (ite (= bv1[1] ?e39) ?e42 ?e32))
+(let (?e44 (bvmul ?e43 ?e5))
+(let (?e45 (bvor ?e44 ?e4))
+(let (?e46 (bvmul ?e44 ?e6))
+(let (?e47 (bvmul ?e46 ?e45))
+(let (?e48 (bvor ?e47 ?e4))
+(let (?e49 (bvshl ?e48 (zero_extend[27] ?e38)))
+(let (?e50 (bvsub ?e38 ?e7))
+(let (?e51 (ite (bvuge ?e41 ?e49) bv1[1] bv0[1]))
+(let (?e52 (bvsub ?e41 ?e49))
+(let (?e53 (ite (= bv1[1] ?e51) ?e52 ?e41))
+(let (?e54 (bvor ?e44 ?e4))
+(let (?e55 (ite (= bv1[1] ?e51) ?e54 ?e44))
+(let (?e56 (bvmul ?e55 ?e5))
+(let (?e57 (bvor ?e56 ?e4))
+(let (?e58 (bvmul ?e56 ?e6))
+(let (?e59 (bvmul ?e58 ?e57))
+(let (?e60 (bvor ?e59 ?e4))
+(let (?e61 (bvshl ?e60 (zero_extend[27] ?e50)))
+(let (?e62 (bvsub ?e50 ?e7))
+(let (?e63 (ite (bvuge ?e53 ?e61) bv1[1] bv0[1]))
+(let (?e64 (bvsub ?e53 ?e61))
+(let (?e65 (ite (= bv1[1] ?e63) ?e64 ?e53))
+(let (?e66 (bvor ?e56 ?e4))
+(let (?e67 (ite (= bv1[1] ?e63) ?e66 ?e56))
+(let (?e68 (bvmul ?e67 ?e5))
+(let (?e69 (bvor ?e68 ?e4))
+(let (?e70 (bvmul ?e68 ?e6))
+(let (?e71 (bvmul ?e70 ?e69))
+(let (?e72 (bvor ?e71 ?e4))
+(let (?e73 (bvshl ?e72 (zero_extend[27] ?e62)))
+(let (?e74 (bvsub ?e62 ?e7))
+(let (?e75 (ite (bvuge ?e65 ?e73) bv1[1] bv0[1]))
+(let (?e76 (bvsub ?e65 ?e73))
+(let (?e77 (ite (= bv1[1] ?e75) ?e76 ?e65))
+(let (?e78 (bvor ?e68 ?e4))
+(let (?e79 (ite (= bv1[1] ?e75) ?e78 ?e68))
+(let (?e80 (bvmul ?e79 ?e5))
+(let (?e81 (bvor ?e80 ?e4))
+(let (?e82 (bvmul ?e80 ?e6))
+(let (?e83 (bvmul ?e82 ?e81))
+(let (?e84 (bvor ?e83 ?e4))
+(let (?e85 (bvshl ?e84 (zero_extend[27] ?e74)))
+(let (?e86 (bvsub ?e74 ?e7))
+(let (?e87 (ite (bvuge ?e77 ?e85) bv1[1] bv0[1]))
+(let (?e88 (bvsub ?e77 ?e85))
+(let (?e89 (ite (= bv1[1] ?e87) ?e88 ?e77))
+(let (?e90 (bvor ?e80 ?e4))
+(let (?e91 (ite (= bv1[1] ?e87) ?e90 ?e80))
+(let (?e92 (bvmul ?e91 ?e5))
+(let (?e93 (bvor ?e92 ?e4))
+(let (?e94 (bvmul ?e92 ?e6))
+(let (?e95 (bvmul ?e94 ?e93))
+(let (?e96 (bvor ?e95 ?e4))
+(let (?e97 (bvshl ?e96 (zero_extend[27] ?e86)))
+(let (?e98 (bvsub ?e86 ?e7))
+(let (?e99 (ite (bvuge ?e89 ?e97) bv1[1] bv0[1]))
+(let (?e100 (bvsub ?e89 ?e97))
+(let (?e101 (ite (= bv1[1] ?e99) ?e100 ?e89))
+(let (?e102 (bvor ?e92 ?e4))
+(let (?e103 (ite (= bv1[1] ?e99) ?e102 ?e92))
+(let (?e104 (bvmul ?e103 ?e5))
+(let (?e105 (bvor ?e104 ?e4))
+(let (?e106 (bvmul ?e104 ?e6))
+(let (?e107 (bvmul ?e106 ?e105))
+(let (?e108 (bvor ?e107 ?e4))
+(let (?e109 (bvshl ?e108 (zero_extend[27] ?e98)))
+(let (?e110 (bvsub ?e98 ?e7))
+(let (?e111 (ite (bvuge ?e101 ?e109) bv1[1] bv0[1]))
+(let (?e112 (bvsub ?e101 ?e109))
+(let (?e113 (ite (= bv1[1] ?e111) ?e112 ?e101))
+(let (?e114 (bvor ?e104 ?e4))
+(let (?e115 (ite (= bv1[1] ?e111) ?e114 ?e104))
+(let (?e116 (bvmul ?e115 ?e5))
+(let (?e117 (bvor ?e116 ?e4))
+(let (?e118 (bvmul ?e116 ?e6))
+(let (?e119 (bvmul ?e118 ?e117))
+(let (?e120 (bvor ?e119 ?e4))
+(let (?e121 (bvshl ?e120 (zero_extend[27] ?e110)))
+(let (?e122 (bvsub ?e110 ?e7))
+(let (?e123 (ite (bvuge ?e113 ?e121) bv1[1] bv0[1]))
+(let (?e124 (bvsub ?e113 ?e121))
+(let (?e125 (ite (= bv1[1] ?e123) ?e124 ?e113))
+(let (?e126 (bvor ?e116 ?e4))
+(let (?e127 (ite (= bv1[1] ?e123) ?e126 ?e116))
+(let (?e128 (bvmul ?e127 ?e5))
+(let (?e129 (bvor ?e128 ?e4))
+(let (?e130 (bvmul ?e128 ?e6))
+(let (?e131 (bvmul ?e130 ?e129))
+(let (?e132 (bvor ?e131 ?e4))
+(let (?e133 (bvshl ?e132 (zero_extend[27] ?e122)))
+(let (?e134 (bvsub ?e122 ?e7))
+(let (?e135 (ite (bvuge ?e125 ?e133) bv1[1] bv0[1]))
+(let (?e136 (bvsub ?e125 ?e133))
+(let (?e137 (ite (= bv1[1] ?e135) ?e136 ?e125))
+(let (?e138 (bvor ?e128 ?e4))
+(let (?e139 (ite (= bv1[1] ?e135) ?e138 ?e128))
+(let (?e140 (bvmul ?e139 ?e139))
+(let (?e141 (bvmul ?e140 ?e139))
+(let (?e142 (ite (= x ?e141) bv1[1] bv0[1]))
+(let (?e143 (bvadd ?e139 bv1[32]))
+(let (?e144 (bvmul ?e143 ?e143))
+(let (?e145 (bvmul ?e144 ?e143))
+(let (?e146 (ite (bvult ?e141 x) bv1[1] bv0[1]))
+(let (?e147 (ite (bvugt ?e145 x) bv1[1] bv0[1]))
+(let (?e148 (bvand ?e146 ?e147))
+(let (?e149 (bvor ?e142 ?e148))
+(not (= (bvnot ?e149) bv0[1]))
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
--- /dev/null
+//g++ -I$(HOME)/stp/c_interface print.c -L$(HOME)/stp/lib -lstp -o hex
+
+#include <stdio.h>
+#include "c_interface.h"
+#include <iostream>
+#include <stdlib.h>
+
+int main() {
+ VC vc = vc_createValidityChecker();
+ vc_setFlags(vc,'m');
+
+ srand(time(NULL));
+ Expr c = vc_parseExpr(vc,"./example.smt");
+
+ for (int i=0; i < 10; i++)
+ {
+ int time = rand() % 7000;
+ std::cout << "Timeout : " << time << " : result " ;
+ std::cout << vc_query(vc,vc_falseExpr(vc),time) << std::endl;
+ }
+ vc_DeleteExpr(c);
+ vc_Destroy(vc);
+}
+
projects / francis / stp.git / commitdiff