From 389c2018df2e3780896497a8b02b8579ea866634 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 3 May 2013 17:30:07 -0700 Subject: [PATCH] working on duality --- src/api/dotnet/Properties/AssemblyInfo.cs | 4 +- src/ast/ast.h | 4 +- src/duality/duality_profiling.cpp | 77 +---------------------- src/duality/duality_solver.cpp | 2 +- src/duality/duality_wrapper.cpp | 10 +++ src/duality/duality_wrapper.h | 6 +- src/muz_qe/duality_dl_interface.cpp | 15 +++-- 7 files changed, 29 insertions(+), 89 deletions(-) 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/ast/ast.h b/src/ast/ast.h index 2753d0006..9c1bfcaf6 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -2295,8 +2295,8 @@ public: } void reset() { - ptr_buffer::iterator it = m_to_unmark.begin(); - ptr_buffer::iterator end = m_to_unmark.end(); + ptr_buffer<::ast>::iterator it = m_to_unmark.begin(); + ptr_buffer<::ast>::iterator end = m_to_unmark.end(); for (; it != end; ++it) { reset_mark(*it); } 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 17638335d..4548e3ca7 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 { @@ -545,6 +546,15 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st a.show(); } + 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 20557e3e2..2fc01e755 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -1281,8 +1281,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 ee1eca712..be776fa53 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 { @@ -230,7 +233,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]); @@ -238,7 +241,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]; @@ -259,10 +262,10 @@ static void print_proof(dl_interface *d, std::ostream& out, Solver::Counterexamp // 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"; } @@ -278,7 +281,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";