diff --git a/src/api/dotnet/Properties/AssemblyInfo.cs b/src/api/dotnet/Properties/AssemblyInfo.cs index 1cd0fe7b8..517349177 100644 --- a/src/api/dotnet/Properties/AssemblyInfo.cs +++ b/src/api/dotnet/Properties/AssemblyInfo.cs @@ -34,6 +34,6 @@ using System.Security.Permissions; // You can specify all the values or you can default the Build and Revision Numbers // by using the '*' as shown below: // [assembly: AssemblyVersion("4.2.0.0")] -[assembly: AssemblyVersion("4.3.2.0")] -[assembly: AssemblyFileVersion("4.3.2.0")] +[assembly: AssemblyVersion("4.3.2.0")] +[assembly: AssemblyFileVersion("4.3.2.0")] diff --git a/src/duality/duality.h b/src/duality/duality.h index e77fbe5c2..c6dfc906d 100644 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -733,8 +733,10 @@ namespace Duality { Term ProjectFormula(std::vector &keep_vec, const Term &f); + public: int SubtermTruth(hash_map &memo, const Term &); + private: void ImplicantRed(hash_map &memo, const Term &f, std::vector &lits, hash_set *done, bool truth, hash_set &dont_cares); diff --git a/src/duality/duality_profiling.cpp b/src/duality/duality_profiling.cpp index b516e03ca..bec32c51a 100755 --- a/src/duality/duality_profiling.cpp +++ b/src/duality/duality_profiling.cpp @@ -25,82 +25,7 @@ Revision History: #include #include -#ifdef WIN32 - -// include "Windows.h" - - -#if 0 -typedef __int64 clock_t; - -static clock_t current_time(){ - LARGE_INTEGER lpPerformanceCount; - lpPerformanceCount.QuadPart = 0; - QueryPerformanceCounter(&lpPerformanceCount); - return lpPerformanceCount.QuadPart; -} - -static void output_time(std::ostream &os, clock_t time){ - LARGE_INTEGER lpFrequency; - lpFrequency.QuadPart = 1; - QueryPerformanceFrequency(&lpFrequency); - os << ((double)time)/lpFrequency.QuadPart; -} -#else - -typedef double clock_t; - -static clock_t current_time(){ - FILETIME lpCreationTime; - FILETIME lpExitTime; - FILETIME lpKernelTime; - FILETIME lpUserTime; - - GetProcessTimes( GetCurrentProcess(), - &lpCreationTime, &lpExitTime, &lpKernelTime, &lpUserTime ); - - - double usr_time = ((double) lpUserTime.dwLowDateTime)/10000000. + - ((double) lpUserTime.dwHighDateTime)/(10000000. * pow(2.0,32.0)); - return usr_time; -} - -static void output_time(std::ostream &os, clock_t time){ - os << time; -} - -#endif - -#else - -#include -#include -#include -#include - -static clock_t current_time(){ -#if 0 - struct tms buf; - times(&buf); - return buf.tms_utime; -#else - struct rusage r; - getrusage(RUSAGE_SELF, &r); - return 1000 * r.ru_utime.tv_sec + r.ru_utime.tv_usec / 1000; -#endif -} - -static void output_time(std::ostream &os, clock_t time){ -#if 0 - os << ((double)time)/sysconf(_SC_CLK_TCK); -#else - os << ((double)time)/1000; -#endif -} - -#endif - - +#include "duality_wrapper.h" namespace Duality { diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index bd02db976..88c9d3d3e 100644 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -1266,7 +1266,7 @@ namespace Duality { DerivationTree dt(this,unwinding,reporter,heuristic,FullExpand); bool res = dt.Derive(unwinding,node,UseUnderapprox); int end_decs = rpfp->CumulativeDecisions(); - std::cout << "decisions: " << (end_decs - start_decs) << std::endl; + // std::cout << "decisions: " << (end_decs - start_decs) << std::endl; last_decisions = end_decs - start_decs; if(res){ cex.tree = dt.tree; diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index 0603b5a4a..fd07173d9 100644 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -24,6 +24,7 @@ Revision History: #include "iz3interp.h" #include "statistics.h" #include "expr_abstract.h" +#include "stopwatch.h" namespace Duality { @@ -554,6 +555,15 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st return res; } + double current_time() + { + static stopwatch sw; + static bool started = false; + if(!started) + sw.start(); + return sw.get_seconds(); + } + } diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index 284d1c527..2fa46ba5a 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -1282,8 +1282,10 @@ namespace Duality { m().inc_ref(a.raw()); return to_expr(a.raw()); } - - + + typedef double clock_t; + clock_t current_time(); + inline void output_time(std::ostream &os, clock_t time){os << time;} }; // to make Duality::ast hashable diff --git a/src/muz_qe/duality_dl_interface.cpp b/src/muz_qe/duality_dl_interface.cpp index 304e5773d..1aee09f3f 100644 --- a/src/muz_qe/duality_dl_interface.cpp +++ b/src/muz_qe/duality_dl_interface.cpp @@ -36,9 +36,12 @@ Revision History: #include "expr_abstract.h" #include "model_smt2_pp.h" +// template class symbol_table; + + #include "duality.h" -using namespace Duality; +// using namespace Duality; namespace Duality { @@ -231,7 +234,7 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp // print the label and the proved fact - out << "(" << node.number; + out << "(step s!" << node.number; out << " (" << node.Name.name(); for(unsigned i = 0; i < edge.F.IndParams.size(); i++) out << " " << cex.tree->Eval(&edge,edge.F.IndParams[i]); @@ -239,7 +242,7 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp // print the substitution - out << " (\n"; + out << " (subst\n"; RPFP::Edge *orig_edge = edge.map; int orig_clause = d->dd()->map[orig_edge]; expr &t = d->dd()->clauses[orig_clause]; @@ -257,14 +260,26 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp } out << " )\n"; + out << " (labels"; + std::vector &labels = d->dd()->clause_labels[orig_clause]; + { + hash_map memo; + for(unsigned j = 0; j < labels.size(); j++){ + RPFP::label_struct &lab = labels[j]; + int truth = cex.tree->SubtermTruth(memo,lab.value); + if(truth == 1 && lab.pos || truth == 0 && !lab.pos) + out << " " << lab.name; + } + } + out << " )\n"; // reference the proofs of all the children, in syntactic order // "true" means the child is not needed - out << " ("; + out << " (ref "; for(unsigned i = 0; i < edge.Children.size(); i++){ if(!cex.tree->Empty(edge.Children[i])) - out << " " << edge.Children[i]->number; + out << " s!" << edge.Children[i]->number; else out << " true"; } @@ -280,7 +295,7 @@ void dl_interface::display_certificate(std::ostream& out) { model_smt2_pp(out, m, *md.get(), 0); } else if(_d->status == StatusRefutation){ - out << "(\n"; + out << "(derivation\n"; // negation of the query is the last clause -- prove it print_proof(this,out,_d->cex); out << ")\n";