From 79121aeeb03bf70323208d5059e23dfb62a83903 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 6 Aug 2018 18:55:29 -0500 Subject: Fixes for sygus inference (#2238) This includes: - Enabling sygus-specific options in SmtEngine::setDefaults, - Disabling a variant of miniscoping (triggered by many chc-comp18 benchmarks), - Treating free constants as functions to synthesize --- src/smt/smt_engine.cpp | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'src/smt') diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 116d2fe23..15b6e2fc9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1403,6 +1403,8 @@ void SmtEngine::setDefaults() { d_logic = d_logic.getUnlockedCopy(); d_logic.enableTheory(THEORY_DATATYPES); d_logic.lock(); + // since we are trying to recast as sygus, we assume the input is sygus + is_sygus = true; } if ((options::checkModels() || options::checkSynthSol()) @@ -2053,6 +2055,10 @@ void SmtEngine::setDefaults() { if( !options::miniscopeQuantFreeVar.wasSetByUser() ){ options::miniscopeQuantFreeVar.set( false ); } + if (!options::quantSplit.wasSetByUser()) + { + options::quantSplit.set(false); + } //rewrite divk if( !options::rewriteDivk.wasSetByUser()) { options::rewriteDivk.set( true ); -- cgit v1.2.3