From 1bf5bc13506ba8c517925a50a6650a594d3ec42d Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 16 Apr 2015 11:21:07 +0200 Subject: Handle (degenerate) case of synthesis conjectures for constants. Disable delta lemmas. --- src/theory/quantifiers/ce_guided_instantiation.cpp | 6 +++++- src/theory/quantifiers/ce_guided_single_inv.cpp | 3 +++ 2 files changed, 8 insertions(+), 1 deletion(-) (limited to 'src/theory/quantifiers') diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 7553eb736..ea97513b8 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -505,7 +505,11 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { } if( !(Trace.isOn("cegqi-stats")) ){ out << "(define-fun " << f << " "; - out << dt.getSygusVarList() << " "; + if( dt.getSygusVarList().isNull() ){ + out << "() "; + }else{ + out << dt.getSygusVarList() << " "; + } out << dt.getSygusType() << " "; if( status==0 ){ out << sol; diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index b3c1e1eaa..a612db872 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -637,6 +637,8 @@ Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std: //check if delta has a lower bound L // if so, add lemma L>0 => L>d void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) { + return; + /* disable for now if( !d_n_delta.isNull() ){ Theory* theory = d_qe->getTheoryEngine()->theoryOf( THEORY_ARITH ); if( theory && d_qe->getTheoryEngine()->isTheoryEnabled( THEORY_ARITH ) ){ @@ -701,6 +703,7 @@ void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) { } } } + */ } void CegInstantiator::check() { -- cgit v1.2.3