From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 26 Feb 2020 20:59:38 +0000 (-0600)
Subject: More fixes for printing sygus commands (#3812)
X-Git-Tag: cvc5-1.0.0~3594
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3ef1df6e974ba572a8def512489cd9e47e9d2a2b;p=cvc5.git

More fixes for printing sygus commands (#3812)

Towards v1 -> v2 sygus conversion.

This makes several fixes and improvements related to printing sygus commands:
(1) The logic is extended with LIA, DT, UF internally during setDefaults instead of during parsing. This is the correct place for this extension of the logic since it should be applied regardless of the parser. 5 existing logic bugs were discovered as a result of this in regressions, which are fixed by this PR.
(2) Ensures that terms in sygus grammars are printed without letification, since this is prohibited in sygus. Notice the formulas printed by constraints need to be letified (otherwise we can't convert large lustre benchmarks). Thus, the letification threshold should determine this but always be overridden for grammar terms.
(3) Ensures final options are set for all sygus-specific commands, which follows the standards prescribed by sygus v2 (all set-* commands come before other commands).
---

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 8faeab491..d915d2ab4 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -755,12 +755,6 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
       warning("Logics in sygus are assumed to contain quantifiers.");
       warning("Omit QF_ from the logic to avoid this warning.");
     }
-    // get unlocked copy, modify, copy and relock
-    LogicInfo log(d_logic.getUnlockedCopy());
-    // enable everything needed for sygus
-    log.enableSygus();
-    d_logic = log;
-    d_logic.lock();
   }
 
   // Core theory belongs to every logic
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 28471de72..886be0cfa 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -84,8 +84,9 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang)
 void Printer::toStreamSygus(std::ostream& out, TNode n) const
 {
   // no sygus-specific printing associated with this printer,
-  // just print the original term
-  toStream(out, n, -1, false, 1);
+  // just print the original term, without letification (the fifth argument is
+  // set to 0).
+  toStream(out, n, -1, false, 0);
 }
 
 void Printer::toStream(std::ostream& out, const Model& m) const
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index e9a4d0a83..6fdbd4adb 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1522,7 +1522,8 @@ void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const
         {
           out << "(";
         }
-        out << dt[cIndex].getSygusOp();
+        // print operator without letification (the fifth argument is set to 0).
+        toStream(out, dt[cIndex].getSygusOp(), -1, false, 0);
         if (n.getNumChildren() > 0)
         {
           for (Node nc : n)
@@ -1537,15 +1538,12 @@ void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const
     }
   }
   Node p = n.getAttribute(theory::SygusPrintProxyAttribute());
-  if (!p.isNull())
+  if (p.isNull())
   {
-    out << p;
-  }
-  else
-  {
-    // cannot convert term to analog, print original
-    out << n;
+    p = n;
   }
+  // cannot convert term to analog, print original, without letification.
+  toStream(out, p, -1, false, 0);
 }
 
 static void toStream(std::ostream& out, const AssertCommand* c)
diff --git a/src/printer/sygus_print_callback.cpp b/src/printer/sygus_print_callback.cpp
index ae1d97c64..92a89a18e 100644
--- a/src/printer/sygus_print_callback.cpp
+++ b/src/printer/sygus_print_callback.cpp
@@ -78,8 +78,9 @@ void SygusExprPrintCallback::toStreamSygus(const Printer* p,
     sbody =
         sbody.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
 
+    // print to stream without letification
     std::stringstream body_out;
-    body_out << sbody;
+    p->toStream(body_out, sbody, -1, false, 0);
 
     // do string substitution
     Assert(e.getNumChildren() == d_args.size());
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 081e36953..915dc603e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1313,13 +1313,18 @@ void SmtEngine::setDefaults() {
     {
       // since we are trying to recast as sygus, we assume the input is sygus
       is_sygus = true;
-      // we change the logic to incorporate sygus immediately
-      d_logic = d_logic.getUnlockedCopy();
-      d_logic.enableSygus();
-      d_logic.lock();
     }
   }
 
+  // We now know whether the input is sygus. Update the logic to incorporate
+  // the theories we need internally for handling sygus problems.
+  if (is_sygus)
+  {
+    d_logic = d_logic.getUnlockedCopy();
+    d_logic.enableSygus();
+    d_logic.lock();
+  }
+
   // sygus core connective requires unsat cores
   if (options::sygusCoreConnective())
   {
@@ -3983,6 +3988,8 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore)
 
 void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type)
 {
+  SmtScope smts(this);
+  finalOptionsAreSet();
   d_private->d_sygusVars.push_back(Node::fromExpr(var));
   Trace("smt") << "SmtEngine::declareSygusVar: " << var << "\n";
   Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type);
@@ -3991,6 +3998,8 @@ void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type)
 
 void SmtEngine::declareSygusPrimedVar(const std::string& id, Type type)
 {
+  SmtScope smts(this);
+  finalOptionsAreSet();
   // do nothing (the command is spurious)
   Trace("smt") << "SmtEngine::declareSygusPrimedVar: " << id << "\n";
   // don't need to set that the conjecture is stale
@@ -4000,6 +4009,8 @@ void SmtEngine::declareSygusFunctionVar(const std::string& id,
                                         Expr var,
                                         Type type)
 {
+  SmtScope smts(this);
+  finalOptionsAreSet();
   d_private->d_sygusVars.push_back(Node::fromExpr(var));
   Trace("smt") << "SmtEngine::declareSygusFunctionVar: " << var << "\n";
   Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type);
@@ -4044,6 +4055,7 @@ void SmtEngine::declareSynthFun(const std::string& id,
 void SmtEngine::assertSygusConstraint(Expr constraint)
 {
   SmtScope smts(this);
+  finalOptionsAreSet();
   d_private->d_sygusConstraints.push_back(constraint);
 
   Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint << "\n";
@@ -4058,6 +4070,7 @@ void SmtEngine::assertSygusInvConstraint(const Expr& inv,
                                          const Expr& post)
 {
   SmtScope smts(this);
+  finalOptionsAreSet();
   // build invariant constraint
 
   // get variables (regular and their respective primed versions)
diff --git a/test/regress/regress0/sygus/sygus-uf.sy b/test/regress/regress0/sygus/sygus-uf.sy
index 1b060637a..d506dd5b2 100644
--- a/test/regress/regress0/sygus/sygus-uf.sy
+++ b/test/regress/regress0/sygus/sygus-uf.sy
@@ -1,6 +1,6 @@
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --sygus-out=status --uf-ho
 ; EXPECT: unsat
-(set-logic LIA)
+(set-logic UFLIA)
 
 (declare-fun uf (Int) Int)
 
diff --git a/test/regress/regress1/sygus/constant-bool-si-all.sy b/test/regress/regress1/sygus/constant-bool-si-all.sy
index eee7956f4..45d49e75b 100644
--- a/test/regress/regress1/sygus/constant-bool-si-all.sy
+++ b/test/regress/regress1/sygus/constant-bool-si-all.sy
@@ -1,6 +1,6 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --sygus-out=status
-(set-logic SAT)
+(set-logic LIA)
 (synth-fun f () Bool)
 (synth-fun g () Bool)
 (synth-fun h () Bool)
diff --git a/test/regress/regress1/sygus/constant-dec-tree-bug.sy b/test/regress/regress1/sygus/constant-dec-tree-bug.sy
index 7229dea2e..e20520a4a 100644
--- a/test/regress/regress1/sygus/constant-dec-tree-bug.sy
+++ b/test/regress/regress1/sygus/constant-dec-tree-bug.sy
@@ -1,7 +1,7 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --sygus-out=status --sygus-unif-pi=complete
 
-(set-logic SAT)
+(set-logic LIA)
 (synth-fun u ((x Int)) Int)
 (synth-fun f () Bool)
 (synth-fun g () Bool)
diff --git a/test/regress/regress1/sygus/sygus-uf-ex.sy b/test/regress/regress1/sygus/sygus-uf-ex.sy
index b9731de0f..66880eafa 100644
--- a/test/regress/regress1/sygus/sygus-uf-ex.sy
+++ b/test/regress/regress1/sygus/sygus-uf-ex.sy
@@ -1,6 +1,6 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
-(set-logic LIA)
+; COMMAND-LINE: --sygus-out=status --uf-ho
+(set-logic UFLIA)
 (declare-fun uf ( Int ) Int)
 (synth-fun f ((x Int) (y Int)) Bool
 ((Start Bool (true false
diff --git a/test/regress/regress1/sygus/tester.sy b/test/regress/regress1/sygus/tester.sy
index bf1cd1576..282bc122c 100644
--- a/test/regress/regress1/sygus/tester.sy
+++ b/test/regress/regress1/sygus/tester.sy
@@ -1,7 +1,7 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --sygus-out=status
 
-(set-logic SLIA)
+(set-logic DTSLIA)
 (declare-datatype DT ((A (a Int)) (B (b String)) (JSBool (jsBool Bool))))
 
 (define-fun isA ((i DT)) Bool ((_ is A) i) )