added z3 problem export synatx feature

vprover · Dec 11, 2024 · f867ded · f867ded
1 parent 0b78e07
commit f867ded
Show file tree

Hide file tree

Showing 11 changed files with 1,062 additions and 224 deletions.
diff --git a/Inferences/TheoryInstAndSimp.cpp b/Inferences/TheoryInstAndSimp.cpp
@@ -69,7 +69,8 @@ TheoryInstAndSimp::TheoryInstAndSimp(Options& opts) : TheoryInstAndSimp(
     opts.thiTautologyDeletion(), 
     opts.showZ3(),  
     opts.thiGeneralise(),
-    opts.exportThiProblem()
+    opts.exportThiProblem(),
+    opts.problemExportSyntax()
     ) {}
 
 
@@ -87,12 +88,12 @@ Options::TheoryInstSimp manageDeprecations(Options::TheoryInstSimp mode)
   }
 }
 
-TheoryInstAndSimp::TheoryInstAndSimp(Options::TheoryInstSimp mode, bool thiTautologyDeletion, bool showZ3, bool generalisation, std::string const& exportSmtlib) 
+TheoryInstAndSimp::TheoryInstAndSimp(Options::TheoryInstSimp mode, bool thiTautologyDeletion, bool showZ3, bool generalisation, std::string const& exportSmtlib, Shell::Options::ProblemExportSyntax problemExportSyntax) 
   : _splitter(0)
   , _mode(manageDeprecations(mode))
   , _thiTautologyDeletion(thiTautologyDeletion)
   , _naming()
-  , _solver(new Z3Interfacing(_naming, showZ3, /* unsatCoresForAssumptions = */ generalisation, exportSmtlib))
+  , _solver(new Z3Interfacing(_naming, showZ3, /* unsatCoresForAssumptions = */ generalisation, exportSmtlib, problemExportSyntax))
   , _generalisation(generalisation)
   , _instantiationConstants ("$inst")
   , _generalizationConstants("$inst$gen")

diff --git a/Inferences/TheoryInstAndSimp.hpp b/Inferences/TheoryInstAndSimp.hpp
@@ -52,7 +52,7 @@ class TheoryInstAndSimp
   TheoryInstAndSimp(TheoryInstAndSimp&&) = default;
 
   TheoryInstAndSimp(Options& opts);
-  TheoryInstAndSimp(Options::TheoryInstSimp mode, bool thiTautologyDeletion, bool showZ3, bool generalisation, std::string const& exportSmtlib);
+  TheoryInstAndSimp(Options::TheoryInstSimp mode, bool thiTautologyDeletion, bool showZ3, bool generalisation, std::string const& exportSmtlib, Shell::Options::ProblemExportSyntax problemExportSyntax);
 
   void attach(SaturationAlgorithm* salg);
 

diff --git a/Kernel/Theory.hpp b/Kernel/Theory.hpp
@@ -54,6 +54,22 @@ class DivByZeroException         : public ArithmeticException
   DivByZeroException() : ArithmeticException("divided by zero"){} 
 };
 
+enum class Sign : uint8_t {
+  Zero = 0,
+  Pos = 1,
+  Neg = 2,
+};
+
+inline std::ostream& operator<<(std::ostream& out, Sign const& self)
+{
+  switch(self) {
+    case Sign::Zero: return out << "0";
+    case Sign::Pos: return out << "+";
+    case Sign::Neg: return out << "-";
+  }
+  ASSERTION_VIOLATION
+}
+
 class IntegerConstantType
 {
 public:
@@ -100,6 +116,11 @@ class IntegerConstantType
 
   InnerType toInner() const { return _val; }
 
+  Sign sign() const 
+  { return _val > 0 ? Sign::Pos
+     : _val < 0 ? Sign::Neg
+     :            Sign::Zero; }
+
   bool isZero(){ return _val==0; }
   bool isNegative(){ return _val<0; }