summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/parser/smt2/smt2.cpp6
-rw-r--r--src/printer/printer.cpp5
-rw-r--r--src/printer/smt2/smt2_printer.cpp14
-rw-r--r--src/printer/sygus_print_callback.cpp3
-rw-r--r--src/smt/smt_engine.cpp21
-rw-r--r--test/regress/regress0/sygus/sygus-uf.sy4
-rw-r--r--test/regress/regress1/sygus/constant-bool-si-all.sy2
-rw-r--r--test/regress/regress1/sygus/constant-dec-tree-bug.sy2
-rw-r--r--test/regress/regress1/sygus/sygus-uf-ex.sy4
-rw-r--r--test/regress/regress1/sygus/tester.sy2
10 files changed, 35 insertions, 28 deletions
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) )
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback