diff options
Diffstat (limited to 'src')
45 files changed, 1202 insertions, 924 deletions
diff --git a/src/base/check.h b/src/base/check.h index 2597807dc..434d38ede 100644 --- a/src/base/check.h +++ b/src/base/check.h @@ -158,7 +158,7 @@ class OstreamVoider #else #define Assert(cond) \ CVC4_FATAL_IF(false, __PRETTY_FUNCTION__, __FILE__, __LINE__) -#endif /* CVC4_DEBUG */ +#endif class AssertArgumentException : public Exception { diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 0ac3ad6bd..e80ed7749 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -18,7 +18,6 @@ # include <sys/resource.h> #endif /* ! __WIN32__ */ -#include <cassert> #include <iostream> #include <memory> #include <string> diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index ecd754bb4..4fe8d4da9 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -17,7 +17,6 @@ #include "main/interactive_shell.h" #include <algorithm> -#include <cassert> #include <cstdlib> #include <iostream> #include <set> @@ -37,6 +36,7 @@ #endif /* HAVE_LIBEDITLINE */ #include "api/cvc4cpp.h" +#include "base/check.h" #include "base/output.h" #include "expr/symbol_manager.h" #include "options/language.h" @@ -222,12 +222,12 @@ restart: Debug("interactive") << "Input now '" << input << line << "'" << endl << flush; - assert( !(d_in.fail() && !d_in.eof()) || line.empty() ); + Assert(!(d_in.fail() && !d_in.eof()) || line.empty()); /* Check for failure. */ if(d_in.fail() && !d_in.eof()) { /* This should only happen if the input line was empty. */ - assert( line.empty() ); + Assert(line.empty()); d_in.clear(); } @@ -262,7 +262,7 @@ restart: { /* Extract the newline delimiter from the stream too */ int c CVC4_UNUSED = d_in.get(); - assert(c == '\n'); + Assert(c == '\n'); Debug("interactive") << "Next char is '" << (char)c << "'" << endl << flush; } diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index a83e10811..d0737bad6 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -19,6 +19,7 @@ #include <antlr3.h> #include <limits.h> +#include "base/check.h" #include "base/output.h" #include "parser/antlr_line_buffered_input.h" #include "parser/bounded_token_buffer.h" @@ -111,7 +112,7 @@ AntlrInputStream::AntlrInputStream(std::string name, pANTLR3_INPUT_STREAM input, d_input(input), d_inputString(inputString), d_line_buffer(line_buffer) { - assert( input != NULL ); + Assert(input != NULL); input->fileName = input->strFactory->newStr8(input->strFactory, (pANTLR3_UINT8)name.c_str()); } @@ -197,8 +198,8 @@ AntlrInputStream::newStreamInputStream(std::istream& input, throw InputStreamException("Stream input failed: " + name); } ptrdiff_t offset = cp - basep; - assert(offset >= 0); - assert(offset <= std::numeric_limits<uint32_t>::max()); + Assert(offset >= 0); + Assert(offset <= std::numeric_limits<uint32_t>::max()); inputStringCopy = (pANTLR3_UINT8)basep; inputStream = newAntrl3InPlaceStream(inputStringCopy, (uint32_t) offset, name); } @@ -217,7 +218,7 @@ AntlrInputStream::newStringInputStream(const std::string& input, const std::string& name) { size_t input_size = input.size(); - assert(input_size <= std::numeric_limits<uint32_t>::max()); + Assert(input_size <= std::numeric_limits<uint32_t>::max()); // Ownership of input_duplicate is transferred to the AntlrInputStream. pANTLR3_UINT8 input_duplicate = (pANTLR3_UINT8) strdup(input.c_str()); @@ -314,11 +315,11 @@ pANTLR3_COMMON_TOKEN_STREAM AntlrInput::getTokenStream() { void AntlrInput::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) { pANTLR3_LEXER lexer = (pANTLR3_LEXER)(recognizer->super); - assert(lexer!=NULL); + Assert(lexer != NULL); Parser *parser = (Parser*)(lexer->super); - assert(parser!=NULL); + Assert(parser != NULL); AntlrInput *input = (AntlrInput*) parser->getInput(); - assert(input!=NULL); + Assert(input != NULL); /* Call the error display routine *if* there's not already a * parse error pending. If a parser error is pending, this diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 411518318..805ac9a48 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -17,17 +17,17 @@ #ifndef CVC4__PARSER__ANTLR_INPUT_H #define CVC4__PARSER__ANTLR_INPUT_H -#include "cvc4parser_private.h" - #include <antlr3.h> + #include <iostream> #include <sstream> #include <stdexcept> #include <string> #include <vector> -#include <cassert> +#include "base/check.h" #include "base/output.h" +#include "cvc4parser_private.h" #include "parser/bounded_token_buffer.h" #include "parser/input.h" #include "parser/line_buffer.h" @@ -249,7 +249,7 @@ inline std::string AntlrInput::tokenTextSubstr(pANTLR3_COMMON_TOKEN token, ANTLR3_MARKER start = token->getStartIndex(token); // Its the last character of the token (not the one just after) ANTLR3_MARKER end = token->getStopIndex(token); - assert( start < end ); + Assert(start < end); if( index > (size_t) end - start ) { std::stringstream ss; ss << "Out-of-bounds substring index: " << index; diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp index 974405a19..121298c4f 100644 --- a/src/parser/antlr_input_imports.cpp +++ b/src/parser/antlr_input_imports.cpp @@ -49,11 +49,11 @@ // (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF // THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. - - #include <antlr3.h> + #include <sstream> +#include "base/check.h" #include "parser/antlr_input.h" #include "parser/parser.h" #include "parser/parser_exception.h" @@ -91,11 +91,11 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { // Dig the CVC4 objects out of the ANTLR3 mess pANTLR3_PARSER antlr3Parser = (pANTLR3_PARSER)(recognizer->super); - assert(antlr3Parser!=NULL); + Assert(antlr3Parser != NULL); Parser *parser = (Parser*)(antlr3Parser->super); - assert(parser!=NULL); + Assert(parser != NULL); AntlrInput *input = (AntlrInput*) parser->getInput() ; - assert(input!=NULL); + Assert(input != NULL); // Signal we are in error recovery now recognizer->state->errorRecovery = ANTLR3_TRUE; @@ -237,7 +237,7 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { } } } else { - assert(false);//("Parse error with empty set of expected tokens."); + Assert(false); //("Parse error with empty set of expected tokens."); } } break; @@ -259,7 +259,7 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { // then we are just going to report what we know about the // token. // - assert(false);//("Unexpected exception in parser."); + Assert(false); //("Unexpected exception in parser."); break; } diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp index 227f15c05..37c38e83b 100644 --- a/src/parser/antlr_line_buffered_input.cpp +++ b/src/parser/antlr_line_buffered_input.cpp @@ -31,10 +31,11 @@ #include "parser/antlr_line_buffered_input.h" #include <antlr3.h> + #include <iostream> #include <string> -#include <cassert> +#include "base/check.h" #include "base/output.h" namespace CVC4 { @@ -284,7 +285,7 @@ static void bufferedInputSeek(pANTLR3_INT_STREAM is, ANTLR3_MARKER seekPoint) { pANTLR3_INPUT_STREAM input = ((pANTLR3_INPUT_STREAM)(is->super)); // Check that we are not seeking backwards. - assert(!((CVC4::parser::pANTLR3_LINE_BUFFERED_INPUT_STREAM)input) + Assert(!((CVC4::parser::pANTLR3_LINE_BUFFERED_INPUT_STREAM)input) ->line_buffer->isPtrBefore( (uint8_t*)seekPoint, input->line, input->charPositionInLine)); @@ -295,20 +296,20 @@ static void bufferedInputSeek(pANTLR3_INT_STREAM is, ANTLR3_MARKER seekPoint) { static ANTLR3_UINT32 bufferedInputSize(pANTLR3_INPUT_STREAM input) { // Not supported for this type of stream - assert(false); + Assert(false); return 0; } static void bufferedInputSetNewLineChar(pANTLR3_INPUT_STREAM input, ANTLR3_UINT32 newlineChar) { // Not supported for this type of stream - assert(false); + Assert(false); } static void bufferedInputSetUcaseLA(pANTLR3_INPUT_STREAM input, ANTLR3_BOOLEAN flag) { // Not supported for this type of stream - assert(false); + Assert(false); } pANTLR3_INPUT_STREAM antlr3LineBufferedStreamNew(std::istream& in, diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp index 3dd2f9168..5db0127c5 100644 --- a/src/parser/bounded_token_buffer.cpp +++ b/src/parser/bounded_token_buffer.cpp @@ -49,12 +49,13 @@ // (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF // THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +#include "parser/bounded_token_buffer.h" + #include <antlr3commontoken.h> #include <antlr3lexer.h> #include <antlr3tokenstream.h> -#include "parser/bounded_token_buffer.h" -#include <cassert> +#include "base/check.h" namespace CVC4 { namespace parser { @@ -138,7 +139,7 @@ pBOUNDED_TOKEN_BUFFER BoundedTokenBufferSourceNew(ANTLR3_UINT32 k, pBOUNDED_TOKEN_BUFFER buffer; pANTLR3_COMMON_TOKEN_STREAM stream; - assert(k > 0); + Assert(k > 0); /* Memory for the interface structure */ buffer = @@ -234,8 +235,7 @@ static pANTLR3_COMMON_TOKEN tokLT(pANTLR3_TOKEN_STREAM ts, ANTLR3_INT32 k) { buffer = (pBOUNDED_TOKEN_BUFFER) cts->super; /* k must be in the range [-buffer->k..buffer->k] */ - assert( k <= (ANTLR3_INT32)buffer->k - && -k <= (ANTLR3_INT32)buffer->k ); + Assert(k <= (ANTLR3_INT32)buffer->k && -k <= (ANTLR3_INT32)buffer->k); if(k == 0) { return NULL; @@ -243,7 +243,7 @@ static pANTLR3_COMMON_TOKEN tokLT(pANTLR3_TOKEN_STREAM ts, ANTLR3_INT32 k) { /* Initialize the buffer on our first call. */ if( __builtin_expect( (buffer->empty == ANTLR3_TRUE), false ) ) { - assert( buffer->tokenBuffer != NULL ); + Assert(buffer->tokenBuffer != NULL); buffer->tokenBuffer[ 0 ] = nextToken(buffer); buffer->maxIndex = 0; buffer->currentIndex = 0; @@ -256,7 +256,7 @@ static pANTLR3_COMMON_TOKEN tokLT(pANTLR3_TOKEN_STREAM ts, ANTLR3_INT32 k) { kIndex = buffer->currentIndex + k - 1; } else { /* Can't look behind more tokens than we've consumed. */ - assert( -k <= (ANTLR3_INT32)buffer->currentIndex ); + Assert(-k <= (ANTLR3_INT32)buffer->currentIndex); /* look-behind token k is at offset -k */ kIndex = buffer->currentIndex + k; } @@ -288,8 +288,8 @@ dbgTokLT (pANTLR3_TOKEN_STREAM ts, ANTLR3_INT32 k) static pANTLR3_COMMON_TOKEN get (pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 i) { - assert(false);// unimplemented - return NULL; + Assert(false); // unimplemented + return NULL; } static pANTLR3_TOKEN_SOURCE @@ -308,21 +308,21 @@ setTokenSource ( pANTLR3_TOKEN_STREAM ts, static pANTLR3_STRING toString (pANTLR3_TOKEN_STREAM ts) { - assert(false);// unimplemented + Assert(false); // unimplemented return NULL; } static pANTLR3_STRING toStringSS(pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 start, ANTLR3_UINT32 stop) { - assert(false);// unimplemented + Assert(false); // unimplemented return NULL; } static pANTLR3_STRING toStringTT (pANTLR3_TOKEN_STREAM ts, pANTLR3_COMMON_TOKEN start, pANTLR3_COMMON_TOKEN stop) { - assert(false);// unimplemented + Assert(false); // unimplemented return NULL; } @@ -382,7 +382,7 @@ _LA (pANTLR3_INT_STREAM is, ANTLR3_INT32 i) static ANTLR3_UINT32 dbgLA (pANTLR3_INT_STREAM is, ANTLR3_INT32 i) { - assert(false); + Assert(false); return 0; } @@ -398,7 +398,7 @@ mark (pANTLR3_INT_STREAM is) static ANTLR3_MARKER dbgMark (pANTLR3_INT_STREAM is) { - assert(false); + Assert(false); return 0; } @@ -411,7 +411,7 @@ release (pANTLR3_INT_STREAM is, ANTLR3_MARKER mark) static ANTLR3_UINT32 size (pANTLR3_INT_STREAM is) { - assert(false); + Assert(false); return 0; } @@ -429,16 +429,8 @@ tindex (pANTLR3_INT_STREAM is) return buffer->currentIndex; } -static void -dbgRewindLast (pANTLR3_INT_STREAM is) -{ - assert(false); -} -static void -rewindLast (pANTLR3_INT_STREAM is) -{ - assert(false); -} +static void dbgRewindLast(pANTLR3_INT_STREAM is) { Assert(false); } +static void rewindLast(pANTLR3_INT_STREAM is) { Assert(false); } static void rewindStream (pANTLR3_INT_STREAM is, ANTLR3_MARKER marker) { @@ -447,7 +439,7 @@ rewindStream (pANTLR3_INT_STREAM is, ANTLR3_MARKER marker) static void dbgRewindStream (pANTLR3_INT_STREAM is, ANTLR3_MARKER marker) { - assert(false); + Assert(false); } static void @@ -464,7 +456,7 @@ seek (pANTLR3_INT_STREAM is, ANTLR3_MARKER index) static void dbgSeek (pANTLR3_INT_STREAM is, ANTLR3_MARKER index) { - assert(false); + Assert(false); } static pANTLR3_COMMON_TOKEN nextToken(pBOUNDED_TOKEN_BUFFER buffer) { diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 0e3e9401b..b7997cafa 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -434,10 +434,10 @@ CVC4::api::Term createPrecedenceTree(Parser* parser, api::Solver* solver, const std::vector<CVC4::api::Term>& expressions, const std::vector<unsigned>& operators, unsigned startIndex, unsigned stopIndex) { - assert(expressions.size() == operators.size() + 1); - assert(startIndex < expressions.size()); - assert(stopIndex < expressions.size()); - assert(startIndex <= stopIndex); + Assert(expressions.size() == operators.size() + 1); + Assert(startIndex < expressions.size()); + Assert(stopIndex < expressions.size()); + Assert(startIndex <= stopIndex); if(stopIndex == startIndex) { return expressions[startIndex]; @@ -544,9 +544,9 @@ api::Term addNots(api::Solver* s, size_t n, api::Term e) { @parser::includes { -#include <cassert> #include <memory> +#include "base/check.h" #include "options/set_language.h" #include "parser/antlr_tracing.h" #include "parser/parser.h" @@ -1134,7 +1134,7 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::api::Sort& t, // like e.g. FORALL(x:INT = 4): [...] PARSER_STATE->parseError("cannot construct a definition here; maybe you want a LET"); } - assert(!idList.empty()); + Assert(!idList.empty()); api::Term fterm = f; std::vector<api::Term> formals; if (f.getKind()==api::LAMBDA) @@ -1210,7 +1210,7 @@ type[CVC4::api::Sort& t, /* a type, possibly a function */ : restrictedTypePossiblyFunctionLHS[t,check,lhs] { if(lhs) { - assert(t.isTuple()); + Assert(t.isTuple()); args = t.getTupleSorts(); } else { args.push_back(t); @@ -2203,12 +2203,12 @@ simpleTerm[CVC4::api::Term& f] } /* bitvector literals */ | HEX_LITERAL - { assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 ); + { Assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 ); std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 4); f = SOLVER->mkBitVector(hexString, 16); } | BINARY_LITERAL - { assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 ); + { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 ); std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4); f = SOLVER->mkBitVector(binString, 2); } @@ -2216,7 +2216,7 @@ simpleTerm[CVC4::api::Term& f] | PARENHASH recordEntry[name,e] { names.push_back(name); args.push_back(e); } ( COMMA recordEntry[name,e] { names.push_back(name); args.push_back(e); } )* HASHPAREN { std::vector< std::pair<std::string, api::Sort> > typeIds; - assert(names.size() == args.size()); + Assert(names.size() == args.size()); for(unsigned i = 0; i < names.size(); ++i) { typeIds.push_back(std::make_pair(names[i], args[i].getSort())); } diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp index 0fe388f01..50a85bf01 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -18,10 +18,11 @@ #include <antlr3.h> +#include "base/check.h" #include "parser/antlr_input.h" -#include "parser/parser_exception.h" #include "parser/cvc/CvcLexer.h" #include "parser/cvc/CvcParser.h" +#include "parser/parser_exception.h" namespace CVC4 { namespace parser { @@ -30,7 +31,7 @@ namespace parser { CvcInput::CvcInput(AntlrInputStream& inputStream) : AntlrInput(inputStream,6) { pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); - assert( input != NULL ); + Assert(input != NULL); d_pCvcLexer = CvcLexerNew(input); if( d_pCvcLexer == NULL ) { @@ -40,7 +41,7 @@ CvcInput::CvcInput(AntlrInputStream& inputStream) : setAntlr3Lexer( d_pCvcLexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); - assert( tokenStream != NULL ); + Assert(tokenStream != NULL); d_pCvcParser = CvcParserNew(tokenStream); if( d_pCvcParser == NULL ) { diff --git a/src/parser/line_buffer.cpp b/src/parser/line_buffer.cpp index 2f7e34852..967503f0f 100644 --- a/src/parser/line_buffer.cpp +++ b/src/parser/line_buffer.cpp @@ -16,11 +16,12 @@ #include "parser/line_buffer.h" -#include <cassert> #include <cstring> #include <iostream> #include <string> +#include "base/check.h" + namespace CVC4 { namespace parser { @@ -36,7 +37,7 @@ uint8_t* LineBuffer::getPtr(size_t line, size_t pos_in_line) { if (!readToLine(line)) { return NULL; } - assert(pos_in_line < d_sizes[line]); + Assert(pos_in_line < d_sizes[line]); return d_lines[line] + pos_in_line; } @@ -49,7 +50,7 @@ uint8_t* LineBuffer::getPtrWithOffset(size_t line, size_t pos_in_line, return getPtrWithOffset(line + 1, 0, offset - (d_sizes[line] - pos_in_line - 1)); } - assert(pos_in_line + offset < d_sizes[line]); + Assert(pos_in_line + offset < d_sizes[line]); return d_lines[line] + pos_in_line + offset; } diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 0309a1f95..086792375 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -16,7 +16,6 @@ #include "parser/parser.h" -#include <cassert> #include <clocale> #include <fstream> #include <iostream> @@ -25,6 +24,7 @@ #include <unordered_set> #include "api/cvc4cpp.h" +#include "base/check.h" #include "base/output.h" #include "expr/kind.h" #include "options/options.h" @@ -75,12 +75,19 @@ api::Solver* Parser::getSolver() const { return d_solver; } api::Term Parser::getSymbol(const std::string& name, SymbolType type) { checkDeclaration(name, CHECK_DECLARED, type); - assert(isDeclared(name, type)); - assert(type == SYM_VARIABLE); + Assert(isDeclared(name, type)); + Assert(type == SYM_VARIABLE); // Functions share var namespace return d_symtab->lookup(name); } +void Parser::forceLogic(const std::string& logic) +{ + Assert(!d_logicIsForced); + d_logicIsForced = true; + d_forcedLogic = logic; +} + api::Term Parser::getVariable(const std::string& name) { return getSymbol(name, SYM_VARIABLE); @@ -100,7 +107,7 @@ api::Term Parser::getExpressionForName(const std::string& name) api::Term Parser::getExpressionForNameAndType(const std::string& name, api::Sort t) { - assert(isDeclared(name)); + Assert(isDeclared(name)); // first check if the variable is declared and not overloaded api::Term expr = getVariable(name); if(expr.isNull()) { @@ -117,7 +124,7 @@ api::Term Parser::getExpressionForNameAndType(const std::string& name, } } // now, post-process the expression - assert( !expr.isNull() ); + Assert(!expr.isNull()); api::Sort te = expr.getSort(); if (te.isConstructor() && te.getConstructorArity() == 0) { @@ -154,7 +161,7 @@ api::Kind Parser::getKindForFunction(api::Term fun) api::Sort Parser::getSort(const std::string& name) { checkDeclaration(name, CHECK_DECLARED, SYM_SORT); - assert(isDeclared(name, SYM_SORT)); + Assert(isDeclared(name, SYM_SORT)); api::Sort t = d_symtab->lookupType(name); return t; } @@ -163,14 +170,14 @@ api::Sort Parser::getSort(const std::string& name, const std::vector<api::Sort>& params) { checkDeclaration(name, CHECK_DECLARED, SYM_SORT); - assert(isDeclared(name, SYM_SORT)); + Assert(isDeclared(name, SYM_SORT)); api::Sort t = d_symtab->lookupType(name, params); return t; } size_t Parser::getArity(const std::string& sort_name) { checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT); - assert(isDeclared(sort_name, SYM_SORT)); + Assert(isDeclared(sort_name, SYM_SORT)); return d_symtab->lookupArity(sort_name); } @@ -263,7 +270,7 @@ void Parser::defineVar(const std::string& name, ss << ", maybe the symbol has already been defined?"; parseError(ss.str()); } - assert(isDeclared(name)); + Assert(isDeclared(name)); } void Parser::defineType(const std::string& name, @@ -273,11 +280,11 @@ void Parser::defineType(const std::string& name, { if (skipExisting && isDeclared(name, SYM_SORT)) { - assert(d_symtab->lookupType(name) == type); + Assert(d_symtab->lookupType(name) == type); return; } d_symtab->bindType(name, type, levelZero); - assert(isDeclared(name, SYM_SORT)); + Assert(isDeclared(name, SYM_SORT)); } void Parser::defineType(const std::string& name, @@ -286,7 +293,7 @@ void Parser::defineType(const std::string& name, bool levelZero) { d_symtab->bindType(name, params, type, levelZero); - assert(isDeclared(name, SYM_SORT)); + Assert(isDeclared(name, SYM_SORT)); } void Parser::defineParameterizedType(const std::string& name, @@ -378,7 +385,7 @@ std::vector<api::Sort> Parser::bindMutualDatatypeTypes( std::vector<api::Sort> types = d_solver->mkDatatypeSorts(datatypes, d_unresolved); - assert(datatypes.size() == types.size()); + Assert(datatypes.size() == types.size()); bool globalDecls = d_symman->getGlobalDeclarations(); for (unsigned i = 0; i < datatypes.size(); ++i) { @@ -611,7 +618,7 @@ bool Parser::isDeclared(const std::string& name, SymbolType type) { case SYM_SORT: return d_symtab->isBoundType(name); } - assert(false); // Unhandled(type); + Assert(false); // Unhandled(type); return false; } @@ -644,8 +651,7 @@ void Parser::checkDeclaration(const std::string& varName, case CHECK_NONE: break; - default: - assert(false); // Unhandled(check); + default: Assert(false); // Unhandled(check); } } diff --git a/src/parser/parser.h b/src/parser/parser.h index abadaea3b..7789fd148 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -19,7 +19,6 @@ #ifndef CVC4__PARSER__PARSER_H #define CVC4__PARSER__PARSER_H -#include <cassert> #include <list> #include <set> #include <string> @@ -271,12 +270,8 @@ public: implementation optional by returning false by default. */ virtual bool logicIsSet() { return false; } - virtual void forceLogic(const std::string& logic) - { - assert(!d_logicIsForced); - d_logicIsForced = true; - d_forcedLogic = logic; - } + virtual void forceLogic(const std::string& logic); + const std::string& getForcedLogic() const { return d_forcedLogic; } bool logicIsForced() const { return d_logicIsForced; } diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 569c63dd0..f47558418 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -15,15 +15,15 @@ **/ // This must be included first. -#include "parser/antlr_input.h" - #include "parser/parser_builder.h" #include <string> #include "api/cvc4cpp.h" +#include "base/check.h" #include "cvc/cvc.h" #include "options/options.h" +#include "parser/antlr_input.h" #include "parser/input.h" #include "parser/parser.h" #include "smt2/smt2.h" @@ -77,11 +77,11 @@ Parser* ParserBuilder::build() input = Input::newFileInput(d_lang, d_filename, d_mmap); break; case LINE_BUFFERED_STREAM_INPUT: - assert( d_streamInput != NULL ); + Assert(d_streamInput != NULL); input = Input::newStreamInput(d_lang, *d_streamInput, d_filename, true); break; case STREAM_INPUT: - assert( d_streamInput != NULL ); + Assert(d_streamInput != NULL); input = Input::newStreamInput(d_lang, *d_streamInput, d_filename); break; case STRING_INPUT: @@ -89,7 +89,7 @@ Parser* ParserBuilder::build() break; } - assert(input != NULL); + Assert(input != NULL); Parser* parser = NULL; switch (d_lang) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 93d0de8f7..e1e1f1cb1 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -77,6 +77,7 @@ using namespace CVC4::parser; #include <memory> +#include "base/check.h" #include "parser/antlr_tracing.h" #include "parser/parse_op.h" #include "parser/parser.h" @@ -1718,13 +1719,13 @@ termAtomic[CVC4::api::Term& atomTerm] // Bit-vector constants | HEX_LITERAL { - assert(AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0); + Assert(AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0); std::string hexStr = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); atomTerm = SOLVER->mkBitVector(hexStr, 16); } | BINARY_LITERAL { - assert(AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0); + Assert(AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0); std::string binStr = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); atomTerm = SOLVER->mkBitVector(binStr, 2); } @@ -1850,7 +1851,7 @@ str[std::string& s, bool fsmtlib] { // Handle SMT-LIB >=2.5 standard escape '""'. ++q; - assert(*q == '"'); + Assert(*q == '"'); } else if (!PARSER_STATE->escapeDupDblQuote() && *q == '\\') { @@ -1858,7 +1859,7 @@ str[std::string& s, bool fsmtlib] // Handle SMT-LIB 2.0 standard escapes '\\' and '\"'. if (*q != '\\' && *q != '"') { - assert(*q != '\0'); + Assert(*q != '\0'); *p++ = '\\'; } } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index df81e6365..a014e1349 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -836,7 +836,7 @@ bool Smt2::isAbstractValue(const std::string& name) api::Term Smt2::mkAbstractValue(const std::string& name) { - assert(isAbstractValue(name)); + Assert(isAbstractValue(name)); // remove the '@' return d_solver->mkAbstractValue(name.substr(1)); } @@ -913,7 +913,7 @@ api::Term Smt2::parseOpToExpr(ParseOp& p) { expr = getExpressionForName(p.d_name); } - assert(!expr.isNull()); + Assert(!expr.isNull()); return expr; } diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 8f53d7b87..c9019811b 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -18,12 +18,13 @@ #include <antlr3.h> +#include "base/check.h" #include "parser/input.h" #include "parser/parser.h" #include "parser/parser_exception.h" -#include "parser/smt2/smt2.h" #include "parser/smt2/Smt2Lexer.h" #include "parser/smt2/Smt2Parser.h" +#include "parser/smt2/smt2.h" namespace CVC4 { namespace parser { @@ -32,7 +33,7 @@ namespace parser { Smt2Input::Smt2Input(AntlrInputStream& inputStream) : AntlrInput(inputStream, 2) { pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); - assert( input != NULL ); + Assert(input != NULL); d_pSmt2Lexer = Smt2LexerNew(input); if( d_pSmt2Lexer == NULL ) { @@ -42,7 +43,7 @@ Smt2Input::Smt2Input(AntlrInputStream& inputStream) : AntlrInput(inputStream, 2) setAntlr3Lexer( d_pSmt2Lexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); - assert( tokenStream != NULL ); + Assert(tokenStream != NULL); d_pSmt2Parser = Smt2ParserNew(tokenStream); if( d_pSmt2Parser == NULL ) { diff --git a/src/parser/smt2/sygus_input.cpp b/src/parser/smt2/sygus_input.cpp index 18320c469..6487e5dd6 100644 --- a/src/parser/smt2/sygus_input.cpp +++ b/src/parser/smt2/sygus_input.cpp @@ -18,12 +18,13 @@ #include <antlr3.h> +#include "base/check.h" #include "parser/input.h" #include "parser/parser.h" #include "parser/parser_exception.h" -#include "parser/smt2/sygus_input.h" #include "parser/smt2/Smt2Lexer.h" #include "parser/smt2/Smt2Parser.h" +#include "parser/smt2/sygus_input.h" namespace CVC4 { namespace parser { @@ -33,7 +34,7 @@ SygusInput::SygusInput(AntlrInputStream& inputStream) : AntlrInput(inputStream, 2) { pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); - assert( input != NULL ); + Assert(input != NULL); d_pSmt2Lexer = Smt2LexerNew(input); if( d_pSmt2Lexer == NULL ) { @@ -43,7 +44,7 @@ SygusInput::SygusInput(AntlrInputStream& inputStream) : setAntlr3Lexer( d_pSmt2Lexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); - assert( tokenStream != NULL ); + Assert(tokenStream != NULL); d_pSmt2Parser = Smt2ParserNew(tokenStream); if( d_pSmt2Parser == NULL ) { diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index aacff46f2..42aac2865 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -21,6 +21,7 @@ #include <set> #include "api/cvc4cpp.h" +#include "base/check.h" #include "options/options.h" #include "parser/parser.h" #include "smt/command.h" @@ -237,7 +238,7 @@ api::Term Tptp::parseOpToExpr(ParseOp& p) } // if it has a kind, it's a builtin one and this function should not have been // called - assert(p.d_kind == api::NULL_EXPR); + Assert(p.d_kind == api::NULL_EXPR); if (isDeclared(p.d_name)) { // already appeared expr = getVariable(p.d_name); @@ -263,7 +264,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args) Debug("parser") << "++ " << *i << std::endl; } } - assert(!args.empty()); + Assert(!args.empty()); // If operator already defined, just build application if (!p.d_expr.isNull()) { @@ -303,7 +304,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args) args[i] = convertRatToUnsorted(args[i]); } } - assert(!v.isNull()); + Assert(!v.isNull()); checkFunctionLike(v); kind = getKindForFunction(v); args.insert(args.begin(), v); @@ -313,7 +314,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args) kind = p.d_kind; isBuiltinKind = true; } - assert(kind != api::NULL_EXPR); + Assert(kind != api::NULL_EXPR); const Options& opts = d_solver->getOptions(); // Second phase: apply parse op to the arguments if (isBuiltinKind) @@ -376,13 +377,13 @@ void Tptp::forceLogic(const std::string& logic) void Tptp::addFreeVar(api::Term var) { - assert(cnf()); + Assert(cnf()); d_freeVar.push_back(var); } std::vector<api::Term> Tptp::getFreeVar() { - assert(cnf()); + Assert(cnf()); std::vector<api::Term> r; r.swap(d_freeVar); return r; @@ -473,7 +474,7 @@ api::Term Tptp::getAssertionExpr(FormulaRole fr, api::Term expr) return d_nullExpr; break; } - assert(false); // unreachable + Assert(false); // unreachable return d_nullExpr; } @@ -501,7 +502,7 @@ Command* Tptp::makeAssertCommand(FormulaRole fr, // "CounterSatisfiable". if (!cnf && (fr == FR_NEGATED_CONJECTURE || fr == FR_CONJECTURE)) { d_hasConjecture = true; - assert(!expr.isNull()); + Assert(!expr.isNull()); } if( expr.isNull() ){ return new EmptyCommand("Untreated role for expression"); diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index ab7746c51..d0459553f 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -21,7 +21,6 @@ #ifndef CVC4__PARSER__TPTP_H #define CVC4__PARSER__TPTP_H -#include <cassert> #include <unordered_map> #include <unordered_set> diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp index 5cb5f6f44..97021b4e9 100644 --- a/src/parser/tptp/tptp_input.cpp +++ b/src/parser/tptp/tptp_input.cpp @@ -18,12 +18,13 @@ #include <antlr3.h> +#include "base/check.h" #include "parser/input.h" #include "parser/parser.h" #include "parser/parser_exception.h" -#include "parser/tptp/tptp.h" #include "parser/tptp/TptpLexer.h" #include "parser/tptp/TptpParser.h" +#include "parser/tptp/tptp.h" namespace CVC4 { namespace parser { @@ -32,7 +33,7 @@ namespace parser { TptpInput::TptpInput(AntlrInputStream& inputStream) : AntlrInput(inputStream, 2) { pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); - assert( input != NULL ); + Assert(input != NULL); d_pTptpLexer = TptpLexerNew(input); if( d_pTptpLexer == NULL ) { @@ -42,7 +43,7 @@ TptpInput::TptpInput(AntlrInputStream& inputStream) : setAntlr3Lexer( d_pTptpLexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); - assert( tokenStream != NULL ); + Assert(tokenStream != NULL); d_pTptpParser = TptpParserNew(tokenStream); if( d_pTptpParser == NULL ) { diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 704ea0e20..3b2b814cd 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -22,9 +22,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <math.h> -#include <vector> #include <iostream> +#include <vector> +#include "base/check.h" #include "base/exception.h" #include "base/output.h" #include "options/bv_options.h" @@ -269,7 +270,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseId& id) void Solver::attachClause(CRef cr) { const Clause& clause = ca[cr]; - assert(clause.size() > 1); + Assert(clause.size() > 1); watches[~clause[0]].push(Watcher(cr, clause[1])); watches[~clause[1]].push(Watcher(cr, clause[0])); if (clause.learnt()) @@ -281,7 +282,7 @@ void Solver::attachClause(CRef cr) { void Solver::detachClause(CRef cr, bool strict) { const Clause& clause = ca[cr]; - assert(clause.size() > 1); + Assert(clause.size() > 1); if (strict) { @@ -396,26 +397,25 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip bool done = false; do{ - assert(confl != CRef_Undef); // (otherwise should be UIP) - Clause& clause = ca[confl]; - - if (clause.learnt()) claBumpActivity(clause); + Assert(confl != CRef_Undef); // (otherwise should be UIP) + Clause& clause = ca[confl]; - for (int j = (p == lit_Undef) ? 0 : 1; j < clause.size(); j++) - { - Lit q = clause[j]; + if (clause.learnt()) claBumpActivity(clause); - if (!seen[var(q)] && level(var(q)) > 0) - { - varBumpActivity(var(q)); - seen[var(q)] = 1; - if (level(var(q)) >= decisionLevel()) - pathC++; - else - out_learnt.push(q); - } + for (int j = (p == lit_Undef) ? 0 : 1; j < clause.size(); j++) + { + Lit q = clause[j]; + if (!seen[var(q)] && level(var(q)) > 0) + { + varBumpActivity(var(q)); + seen[var(q)] = 1; + if (level(var(q)) >= decisionLevel()) + pathC++; + else + out_learnt.push(q); } + } // Select next clause to look at: while (!seen[var(trail[index--])]); @@ -530,7 +530,7 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels) int top = analyze_toclear.size(); while (analyze_stack.size() > 0){ CRef c_reason = reason(var(analyze_stack.last())); - assert(c_reason != CRef_Undef); + Assert(c_reason != CRef_Undef); Clause& clause = ca[c_reason]; int c_size = clause.size(); analyze_stack.pop(); @@ -569,9 +569,9 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels) * @param out_conflict the conflict in terms of assumptions we are building */ void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) { - assert (confl_clause != CRef_Undef); - assert (decisionLevel() == assumptions.size()); - assert (level(var(p)) == assumptions.size()); + Assert(confl_clause != CRef_Undef); + Assert(decisionLevel() == assumptions.size()); + Assert(level(var(p)) == assumptions.size()); out_conflict.clear(); @@ -588,7 +588,7 @@ void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) { // we skip p if was a learnt unit if (x != var(p)) { if (marker[x] == 2) { - assert (level(x) > 0); + Assert(level(x) > 0); out_conflict.push(~trail[i]); } } @@ -602,9 +602,9 @@ void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) { } seen[x] = 0; } - assert(seen[x] == 0); + Assert(seen[x] == 0); } - assert(out_conflict.size()); + Assert(out_conflict.size()); } /*_________________________________________________________________________________________________ @@ -635,8 +635,8 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) Var x = var(trail[i]); if (seen[x]) { if (reason(x) == CRef_Undef) { - assert(marker[x] == 2); - assert(level(x) > 0); + Assert(marker[x] == 2); + Assert(level(x) > 0); if (~trail[i] != p) { out_conflict.push(~trail[i]); @@ -656,23 +656,25 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) } seen[var(p)] = 0; - assert (out_conflict.size()); + Assert(out_conflict.size()); } void Solver::uncheckedEnqueue(Lit p, CRef from) { - assert(value(p) == l_Undef); - assigns[var(p)] = lbool(!sign(p)); - vardata[var(p)] = mkVarData(from, decisionLevel()); - trail.push_(p); - if (decisionLevel() <= assumptions.size() && marker[var(p)] == 1) { - if (d_notify) { - Debug("bvminisat::explain") - << OUTPUT_TAG << "propagating " << p << std::endl; - d_notify->notify(p); - } + Assert(value(p) == l_Undef); + assigns[var(p)] = lbool(!sign(p)); + vardata[var(p)] = mkVarData(from, decisionLevel()); + trail.push_(p); + if (decisionLevel() <= assumptions.size() && marker[var(p)] == 1) + { + if (d_notify) + { + Debug("bvminisat::explain") + << OUTPUT_TAG << "propagating " << p << std::endl; + d_notify->notify(p); } + } } void Solver::popAssumption() { @@ -691,7 +693,7 @@ lbool Solver::assertAssumption(Lit p, bool propagate) { // TODO need to somehow mark the assumption as unit in the current context? // it's not always unit though, but this would be useful for debugging - // assert(marker[var(p)] == 1); + // Assert(marker[var(p)] == 1); if (decisionLevel() > assumptions.size()) { cancelUntil(assumptions.size()); @@ -762,7 +764,7 @@ CRef Solver::propagate() Lit false_lit = ~p; if (clause[0] == false_lit) clause[0] = clause[1], clause[1] = false_lit; - assert(clause[1] == false_lit); + Assert(clause[1] == false_lit); i++; // If 0th watch is true, then clause is already satisfied. @@ -878,27 +880,27 @@ but more things can be put here. |________________________________________________________________________________________________@*/ bool Solver::simplify() { - assert(decisionLevel() == 0); + Assert(decisionLevel() == 0); - if (!ok || propagate() != CRef_Undef) - return ok = false; + if (!ok || propagate() != CRef_Undef) return ok = false; - if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) - return true; + if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) return true; - d_notify->spendResource(ResourceManager::Resource::BvSatSimplifyStep); + d_notify->spendResource(ResourceManager::Resource::BvSatSimplifyStep); - // Remove satisfied clauses: - removeSatisfied(learnts); - if (remove_satisfied) // Can be turned off. - removeSatisfied(clauses); - checkGarbage(); - rebuildOrderHeap(); + // Remove satisfied clauses: + removeSatisfied(learnts); + if (remove_satisfied) // Can be turned off. + removeSatisfied(clauses); + checkGarbage(); + rebuildOrderHeap(); - simpDB_assigns = nAssigns(); - simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now) + simpDB_assigns = nAssigns(); + simpDB_props = + clauses_literals + learnts_literals; // (shouldn't depend on stats + // really, but it will do for now) - return true; + return true; } /*_________________________________________________________________________________________________ @@ -917,176 +919,207 @@ unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached. |________________________________________________________________________________________________@*/ lbool Solver::search(int nof_conflicts, UIP uip) { - assert(ok); - int backtrack_level; - int conflictC = 0; - vec<Lit> learnt_clause; - starts++; - - for (;;){ - d_notify->safePoint(ResourceManager::Resource::BvSatPropagateStep); - CRef confl = propagate(); - if (confl != CRef_Undef){ - // CONFLICT - conflicts++; conflictC++; - - if (decisionLevel() == 0) { - // can this happen for bv? - return l_False; - } + Assert(ok); + int backtrack_level; + int conflictC = 0; + vec<Lit> learnt_clause; + starts++; - learnt_clause.clear(); - analyze(confl, learnt_clause, backtrack_level, uip); + for (;;) + { + d_notify->safePoint(ResourceManager::Resource::BvSatPropagateStep); + CRef confl = propagate(); + if (confl != CRef_Undef) + { + // CONFLICT + conflicts++; + conflictC++; - Lit p = learnt_clause[0]; - //bool assumption = marker[var(p)] == 2; + if (decisionLevel() == 0) + { + // can this happen for bv? + return l_False; + } - CRef cr = CRef_Undef; - if (learnt_clause.size() > 1) { - cr = ca.alloc(learnt_clause, true); - learnts.push(cr); - attachClause(cr); - claBumpActivity(ca[cr]); - } + learnt_clause.clear(); + analyze(confl, learnt_clause, backtrack_level, uip); - if (learnt_clause.size() == 1) { - // learning a unit clause - } + Lit p = learnt_clause[0]; + // bool assumption = marker[var(p)] == 2; - // if the uip was an assumption we are unsat - if (level(var(p)) <= assumptions.size()) { - for (int i = 0; i < learnt_clause.size(); ++i) { - assert(level(var(learnt_clause[i])) <= decisionLevel()); - seen[var(learnt_clause[i])] = 1; - } + CRef cr = CRef_Undef; + if (learnt_clause.size() > 1) + { + cr = ca.alloc(learnt_clause, true); + learnts.push(cr); + attachClause(cr); + claBumpActivity(ca[cr]); + } - analyzeFinal(p, conflict); - Debug("bvminisat::search") << OUTPUT_TAG << " conflict on assumptions " << std::endl; - return l_False; - } + if (learnt_clause.size() == 1) + { + // learning a unit clause + } - if (!CVC4::options::bvEagerExplanations()) { - // check if uip leads to a conflict - if (backtrack_level < assumptions.size()) { - cancelUntil(assumptions.size()); - uncheckedEnqueue(p, cr); - - CRef new_confl = propagate(); - if (new_confl != CRef_Undef) { - // we have a conflict we now need to explain it - analyzeFinal2(p, new_confl, conflict); - return l_False; - } - } - } + // if the uip was an assumption we are unsat + if (level(var(p)) <= assumptions.size()) + { + for (int i = 0; i < learnt_clause.size(); ++i) + { + Assert(level(var(learnt_clause[i])) <= decisionLevel()); + seen[var(learnt_clause[i])] = 1; + } - cancelUntil(backtrack_level); - uncheckedEnqueue(p, cr); - - varDecayActivity(); - claDecayActivity(); - - if (--learntsize_adjust_cnt == 0){ - learntsize_adjust_confl *= learntsize_adjust_inc; - learntsize_adjust_cnt = (int)learntsize_adjust_confl; - max_learnts *= learntsize_inc; - - if (verbosity >= 1) - printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", - (int)conflicts, - (int)dec_vars - - (trail_lim.size() == 0 ? trail.size() - : trail_lim[0]), - nClauses(), - (int)clauses_literals, - (int)max_learnts, - nLearnts(), - (double)learnts_literals / nLearnts(), - progressEstimate() * 100); - } + analyzeFinal(p, conflict); + Debug("bvminisat::search") + << OUTPUT_TAG << " conflict on assumptions " << std::endl; + return l_False; + } - }else{ - // NO CONFLICT - bool isWithinBudget; - try { - isWithinBudget = - withinBudget(ResourceManager::Resource::BvSatConflictsStep); - } - catch (const CVC4::theory::Interrupted& e) { - // do some clean-up and rethrow - cancelUntil(assumptions.size()); - throw e; - } + if (!CVC4::options::bvEagerExplanations()) + { + // check if uip leads to a conflict + if (backtrack_level < assumptions.size()) + { + cancelUntil(assumptions.size()); + uncheckedEnqueue(p, cr); - if ((decisionLevel() > assumptions.size() && nof_conflicts >= 0 - && conflictC >= nof_conflicts) - || !isWithinBudget) - { - // Reached bound on number of conflicts: - Debug("bvminisat::search") - << OUTPUT_TAG << " restarting " << std::endl; - progress_estimate = progressEstimate(); - cancelUntil(assumptions.size()); - return l_Undef; - } + CRef new_confl = propagate(); + if (new_confl != CRef_Undef) + { + // we have a conflict we now need to explain it + analyzeFinal2(p, new_confl, conflict); + return l_False; + } + } + } - // Simplify the set of problem clauses: - if (decisionLevel() == 0 && !simplify()) { - Debug("bvminisat::search") << OUTPUT_TAG << " base level conflict, we're unsat" << std::endl; - return l_False; - } + cancelUntil(backtrack_level); + uncheckedEnqueue(p, cr); - // We can't erase clauses if there is unprocessed assumptions, there might be some - // propagationg we need to redu - if (decisionLevel() >= assumptions.size() && learnts.size()-nAssigns() >= max_learnts) { - // Reduce the set of learnt clauses: - Debug("bvminisat::search") << OUTPUT_TAG << " cleaning up database" << std::endl; - reduceDB(); - } + varDecayActivity(); + claDecayActivity(); - Lit next = lit_Undef; - while (decisionLevel() < assumptions.size()){ - // Perform user provided assumption: - Lit p = assumptions[decisionLevel()]; - if (value(p) == l_True){ - // Dummy decision level: - newDecisionLevel(); - }else if (value(p) == l_False){ - marker[var(p)] = 2; - - analyzeFinal(~p, conflict); - Debug("bvminisat::search") << OUTPUT_TAG << " assumption false, we're unsat" << std::endl; - return l_False; - }else{ - marker[var(p)] = 2; - next = p; - break; - } - } + if (--learntsize_adjust_cnt == 0) + { + learntsize_adjust_confl *= learntsize_adjust_inc; + learntsize_adjust_cnt = (int)learntsize_adjust_confl; + max_learnts *= learntsize_inc; + + if (verbosity >= 1) + printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", + (int)conflicts, + (int)dec_vars + - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), + nClauses(), + (int)clauses_literals, + (int)max_learnts, + nLearnts(), + (double)learnts_literals / nLearnts(), + progressEstimate() * 100); + } + } + else + { + // NO CONFLICT + bool isWithinBudget; + try + { + isWithinBudget = + withinBudget(ResourceManager::Resource::BvSatConflictsStep); + } + catch (const CVC4::theory::Interrupted& e) + { + // do some clean-up and rethrow + cancelUntil(assumptions.size()); + throw e; + } - if (next == lit_Undef){ + if ((decisionLevel() > assumptions.size() && nof_conflicts >= 0 + && conflictC >= nof_conflicts) + || !isWithinBudget) + { + // Reached bound on number of conflicts: + Debug("bvminisat::search") << OUTPUT_TAG << " restarting " << std::endl; + progress_estimate = progressEstimate(); + cancelUntil(assumptions.size()); + return l_Undef; + } - if (only_bcp) { - Debug("bvminisat::search") << OUTPUT_TAG << " only bcp, skipping rest of the problem" << std::endl; - return l_True; - } + // Simplify the set of problem clauses: + if (decisionLevel() == 0 && !simplify()) + { + Debug("bvminisat::search") + << OUTPUT_TAG << " base level conflict, we're unsat" << std::endl; + return l_False; + } - // New variable decision: - decisions++; - next = pickBranchLit(); + // We can't erase clauses if there is unprocessed assumptions, there might + // be some propagationg we need to redu + if (decisionLevel() >= assumptions.size() + && learnts.size() - nAssigns() >= max_learnts) + { + // Reduce the set of learnt clauses: + Debug("bvminisat::search") + << OUTPUT_TAG << " cleaning up database" << std::endl; + reduceDB(); + } - if (next == lit_Undef) { - Debug("bvminisat::search") << OUTPUT_TAG << " satisfiable" << std::endl; - // Model found: - return l_True; - } - } + Lit next = lit_Undef; + while (decisionLevel() < assumptions.size()) + { + // Perform user provided assumption: + Lit p = assumptions[decisionLevel()]; + if (value(p) == l_True) + { + // Dummy decision level: + newDecisionLevel(); + } + else if (value(p) == l_False) + { + marker[var(p)] = 2; - // Increase decision level and enqueue 'next' - newDecisionLevel(); - uncheckedEnqueue(next); + analyzeFinal(~p, conflict); + Debug("bvminisat::search") + << OUTPUT_TAG << " assumption false, we're unsat" << std::endl; + return l_False; } + else + { + marker[var(p)] = 2; + next = p; + break; + } + } + + if (next == lit_Undef) + { + if (only_bcp) + { + Debug("bvminisat::search") + << OUTPUT_TAG << " only bcp, skipping rest of the problem" + << std::endl; + return l_True; + } + + // New variable decision: + decisions++; + next = pickBranchLit(); + + if (next == lit_Undef) + { + Debug("bvminisat::search") + << OUTPUT_TAG << " satisfiable" << std::endl; + // Model found: + return l_True; + } + } + + // Increase decision level and enqueue 'next' + newDecisionLevel(); + uncheckedEnqueue(next); } + } } @@ -1202,7 +1235,7 @@ void Solver::explain(Lit p, std::vector<Lit>& explanation) { if (seen[x]) { if (reason(x) == CRef_Undef) { if (marker[x] == 2) { - assert(level(x) > 0); + Assert(level(x) > 0); explanation.push_back(trail[i]); } else { Assert(level(x) == 0); @@ -1290,8 +1323,11 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps) fprintf(f, "p cnf %d %d\n", max, cnt); for (int i = 0; i < assumps.size(); i++){ - assert(value(assumps[i]) != l_False); - fprintf(f, "%s%d 0\n", sign(assumps[i]) ? "-" : "", mapVar(var(assumps[i]), map, max)+1); + Assert(value(assumps[i]) != l_False); + fprintf(f, + "%s%d 0\n", + sign(assumps[i]) ? "-" : "", + mapVar(var(assumps[i]), map, max) + 1); } for (int i = 0; i < clauses.size(); i++) diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index f2721c88d..03c46985b 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <vector> +#include "base/check.h" #include "context/context.h" #include "proof/clause_id.h" #include "prop/bvminisat/core/SolverTypes.h" @@ -391,8 +392,16 @@ public: //================================================================================================= // Implementation of inline methods: -inline CRef Solver::reason(Var x) const { assert(x < vardata.size()); return vardata[x].reason; } -inline int Solver::level (Var x) const { assert(x < vardata.size()); return vardata[x].level; } +inline CRef Solver::reason(Var x) const +{ + Assert(x < vardata.size()); + return vardata[x].reason; +} +inline int Solver::level(Var x) const +{ + Assert(x < vardata.size()); + return vardata[x].level; +} inline void Solver::insertVarOrder(Var x) { if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); } diff --git a/src/prop/bvminisat/core/SolverTypes.h b/src/prop/bvminisat/core/SolverTypes.h index cf9ce7e15..776052848 100644 --- a/src/prop/bvminisat/core/SolverTypes.h +++ b/src/prop/bvminisat/core/SolverTypes.h @@ -21,13 +21,12 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef BVMinisat_SolverTypes_h #define BVMinisat_SolverTypes_h -#include <assert.h> - -#include "prop/bvminisat/mtl/IntTypes.h" +#include "base/check.h" #include "prop/bvminisat/mtl/Alg.h" -#include "prop/bvminisat/mtl/Vec.h" -#include "prop/bvminisat/mtl/Map.h" #include "prop/bvminisat/mtl/Alloc.h" +#include "prop/bvminisat/mtl/IntTypes.h" +#include "prop/bvminisat/mtl/Map.h" +#include "prop/bvminisat/mtl/Vec.h" namespace CVC4 { namespace BVMinisat { @@ -176,15 +175,20 @@ class Clause { public: void calcAbstraction() { - assert(header.has_extra); - uint32_t abstraction = 0; - for (int i = 0; i < size(); i++) - abstraction |= 1 << (var(data[i].lit) & 31); - data[header.size].abs = abstraction; } - + Assert(header.has_extra); + uint32_t abstraction = 0; + for (int i = 0; i < size(); i++) + abstraction |= 1 << (var(data[i].lit) & 31); + data[header.size].abs = abstraction; + } int size () const { return header.size; } - void shrink (int i) { assert(i <= size()); if (header.has_extra) data[header.size-i] = data[header.size]; header.size -= i; } + void shrink(int i) + { + Assert(i <= size()); + if (header.has_extra) data[header.size - i] = data[header.size]; + header.size -= i; + } void pop () { shrink(1); } bool learnt () const { return header.learnt; } bool has_extra () const { return header.has_extra; } @@ -202,8 +206,16 @@ public: Lit operator [] (int i) const { return data[i].lit; } operator const Lit* (void) const { return (Lit*)data; } - float& activity () { assert(header.has_extra); return data[header.size].act; } - uint32_t abstraction () const { assert(header.has_extra); return data[header.size].abs; } + float& activity() + { + Assert(header.has_extra); + return data[header.size].act; + } + uint32_t abstraction() const + { + Assert(header.has_extra); + return data[header.size].abs; + } Lit subsumes (const Clause& other) const; void strengthen (Lit p); @@ -234,14 +246,15 @@ class ClauseAllocator : public RegionAllocator<uint32_t> template<class Lits> CRef alloc(const Lits& ps, bool learnt = false) { - assert(sizeof(Lit) == sizeof(uint32_t)); - assert(sizeof(float) == sizeof(uint32_t)); - bool use_extra = learnt | extra_clause_field; + Assert(sizeof(Lit) == sizeof(uint32_t)); + Assert(sizeof(float) == sizeof(uint32_t)); + bool use_extra = learnt | extra_clause_field; - CRef cid = RegionAllocator<uint32_t>::alloc(clauseWord32Size(ps.size(), use_extra)); - new (lea(cid)) Clause(ps, use_extra, learnt); + CRef cid = RegionAllocator<uint32_t>::alloc( + clauseWord32Size(ps.size(), use_extra)); + new (lea(cid)) Clause(ps, use_extra, learnt); - return cid; + return cid; } // Deref, Load Effective Address (LEA), Inverse of LEA (AEL): @@ -378,8 +391,10 @@ inline Lit Clause::subsumes(const Clause& other) const { //if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0) //if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0)) - assert(!header.learnt); assert(!other.header.learnt); - assert(header.has_extra); assert(other.header.has_extra); + Assert(!header.learnt); + Assert(!other.header.learnt); + Assert(header.has_extra); + Assert(other.header.has_extra); if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0) return lit_Error; diff --git a/src/prop/bvminisat/mtl/Alg.h b/src/prop/bvminisat/mtl/Alg.h index e61dbb415..5918b2f4c 100644 --- a/src/prop/bvminisat/mtl/Alg.h +++ b/src/prop/bvminisat/mtl/Alg.h @@ -21,6 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef BVMinisat_Alg_h #define BVMinisat_Alg_h +#include "base/check.h" #include "prop/bvminisat/mtl/Vec.h" namespace CVC4 { @@ -38,7 +39,7 @@ static inline void remove(V& ts, const T& t) { int j = 0; for (; j < ts.size() && ts[j] != t; j++); - assert(j < ts.size()); + Assert(j < ts.size()); for (; j < ts.size()-1; j++) ts[j] = ts[j+1]; ts.pop(); } diff --git a/src/prop/bvminisat/mtl/Alloc.h b/src/prop/bvminisat/mtl/Alloc.h index 4e58ab159..8a03caa69 100644 --- a/src/prop/bvminisat/mtl/Alloc.h +++ b/src/prop/bvminisat/mtl/Alloc.h @@ -21,8 +21,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef BVMinisat_Alloc_h #define BVMinisat_Alloc_h -#include "prop/bvminisat/mtl/XAlloc.h" +#include "base/check.h" #include "prop/bvminisat/mtl/Vec.h" +#include "prop/bvminisat/mtl/XAlloc.h" namespace CVC4 { namespace BVMinisat { @@ -61,13 +62,33 @@ class RegionAllocator void free (int size) { wasted_ += size; } // Deref, Load Effective Address (LEA), Inverse of LEA (AEL): - T& operator[](Ref r) { assert(r >= 0 && r < sz); return memory[r]; } - const T& operator[](Ref r) const { assert(r >= 0 && r < sz); return memory[r]; } + T& operator[](Ref r) + { + Assert(r >= 0 && r < sz); + return memory[r]; + } + const T& operator[](Ref r) const + { + Assert(r >= 0 && r < sz); + return memory[r]; + } - T* lea (Ref r) { assert(r >= 0 && r < sz); return &memory[r]; } - const T* lea (Ref r) const { assert(r >= 0 && r < sz); return &memory[r]; } - Ref ael (const T* t) { assert((void*)t >= (void*)&memory[0] && (void*)t < (void*)&memory[sz-1]); - return (Ref)(t - &memory[0]); } + T* lea(Ref r) + { + Assert(r >= 0 && r < sz); + return &memory[r]; + } + const T* lea(Ref r) const + { + Assert(r >= 0 && r < sz); + return &memory[r]; + } + Ref ael(const T* t) + { + Assert((void*)t >= (void*)&memory[0] + && (void*)t < (void*)&memory[sz - 1]); + return (Ref)(t - &memory[0]); + } void moveTo(RegionAllocator& to) { if (to.memory != NULL) ::free(to.memory); @@ -102,7 +123,7 @@ void RegionAllocator<T>::capacity(uint32_t min_cap) } // printf(" .. (%p) cap = %u\n", this, cap); - assert(cap > 0); + Assert(cap > 0); memory = (T*)xrealloc(memory, sizeof(T)*cap); } @@ -112,7 +133,7 @@ typename RegionAllocator<T>::Ref RegionAllocator<T>::alloc(int size) { // printf("ALLOC called (this = %p, size = %d)\n", this, size); fflush(stdout); - assert(size > 0); + Assert(size > 0); capacity(sz + size); uint32_t prev_sz = sz; diff --git a/src/prop/bvminisat/mtl/Heap.h b/src/prop/bvminisat/mtl/Heap.h index 2d7ee0199..38b47bc7f 100644 --- a/src/prop/bvminisat/mtl/Heap.h +++ b/src/prop/bvminisat/mtl/Heap.h @@ -21,6 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef BVMinisat_Heap_h #define BVMinisat_Heap_h +#include "base/check.h" #include "prop/bvminisat/mtl/Vec.h" namespace CVC4 { @@ -79,12 +80,22 @@ class Heap { int size () const { return heap.size(); } bool empty () const { return heap.size() == 0; } bool inHeap (int n) const { return n < indices.size() && indices[n] >= 0; } - int operator[](int index) const { assert(index < heap.size()); return heap[index]; } - - - void decrease (int n) { assert(inHeap(n)); percolateUp (indices[n]); } - void increase (int n) { assert(inHeap(n)); percolateDown(indices[n]); } + int operator[](int index) const + { + Assert(index < heap.size()); + return heap[index]; + } + void decrease(int n) + { + Assert(inHeap(n)); + percolateUp(indices[n]); + } + void increase(int n) + { + Assert(inHeap(n)); + percolateDown(indices[n]); + } // Safe variant of insert/decrease/increase: void update(int n) @@ -100,7 +111,7 @@ class Heap { void insert(int n) { indices.growTo(n+1, -1); - assert(!inHeap(n)); + Assert(!inHeap(n)); indices[n] = heap.size(); heap.push(n); diff --git a/src/prop/bvminisat/mtl/Map.h b/src/prop/bvminisat/mtl/Map.h index ee68a2155..919149fa9 100644 --- a/src/prop/bvminisat/mtl/Map.h +++ b/src/prop/bvminisat/mtl/Map.h @@ -20,6 +20,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef BVMinisat_Map_h #define BVMinisat_Map_h +#include "base/check.h" #include "prop/bvminisat/mtl/IntTypes.h" #include "prop/bvminisat/mtl/Vec.h" @@ -68,8 +69,8 @@ class Map { int size; // Don't allow copying (error prone): - Map<K,D,H,E>& operator = (Map<K,D,H,E>& other) { assert(0); } - Map (Map<K,D,H,E>& other) { assert(0); } + Map<K, D, H, E>& operator=(Map<K, D, H, E>& other) { Assert(0); } + Map(Map<K, D, H, E>& other) { Assert(0); } bool checkCap(int new_size) const { return new_size > cap; } @@ -108,27 +109,25 @@ class Map { // PRECONDITION: the key must already exist in the map. const D& operator [] (const K& k) const { - assert(size != 0); - const D* res = NULL; - const vec<Pair>& ps = table[index(k)]; - for (int i = 0; i < ps.size(); i++) - if (equals(ps[i].key, k)) - res = &ps[i].data; - assert(res != NULL); - return *res; + Assert(size != 0); + const D* res = NULL; + const vec<Pair>& ps = table[index(k)]; + for (int i = 0; i < ps.size(); i++) + if (equals(ps[i].key, k)) res = &ps[i].data; + Assert(res != NULL); + return *res; } // PRECONDITION: the key must already exist in the map. D& operator [] (const K& k) { - assert(size != 0); - D* res = NULL; - vec<Pair>& ps = table[index(k)]; - for (int i = 0; i < ps.size(); i++) - if (equals(ps[i].key, k)) - res = &ps[i].data; - assert(res != NULL); - return *res; + Assert(size != 0); + D* res = NULL; + vec<Pair>& ps = table[index(k)]; + for (int i = 0; i < ps.size(); i++) + if (equals(ps[i].key, k)) res = &ps[i].data; + Assert(res != NULL); + return *res; } // PRECONDITION: the key must *NOT* exist in the map. @@ -154,14 +153,15 @@ class Map { // PRECONDITION: the key must exist in the map. void remove(const K& k) { - assert(table != NULL); - vec<Pair>& ps = table[index(k)]; - int j = 0; - for (; j < ps.size() && !equals(ps[j].key, k); j++); - assert(j < ps.size()); - ps[j] = ps.last(); - ps.pop(); - size--; + Assert(table != NULL); + vec<Pair>& ps = table[index(k)]; + int j = 0; + for (; j < ps.size() && !equals(ps[j].key, k); j++) + ; + Assert(j < ps.size()); + ps[j] = ps.last(); + ps.pop(); + size--; } void clear () { diff --git a/src/prop/bvminisat/mtl/Queue.h b/src/prop/bvminisat/mtl/Queue.h index c40f2322b..1120188f8 100644 --- a/src/prop/bvminisat/mtl/Queue.h +++ b/src/prop/bvminisat/mtl/Queue.h @@ -21,6 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef BVMinisat_Queue_h #define BVMinisat_Queue_h +#include "base/check.h" #include "prop/bvminisat/mtl/Vec.h" namespace CVC4 { @@ -42,11 +43,30 @@ public: void clear (bool dealloc = false) { buf.clear(dealloc); buf.growTo(1); first = end = 0; } int size () const { return (end >= first) ? end - first : end - first + buf.size(); } - const T& operator [] (int index) const { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; } - T& operator [] (int index) { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; } + const T& operator[](int index) const + { + Assert(index >= 0); + Assert(index < size()); + return buf[(first + index) % buf.size()]; + } + T& operator[](int index) + { + Assert(index >= 0); + Assert(index < size()); + return buf[(first + index) % buf.size()]; + } - T peek () const { assert(first != end); return buf[first]; } - void pop () { assert(first != end); first++; if (first == buf.size()) first = 0; } + T peek() const + { + Assert(first != end); + return buf[first]; + } + void pop() + { + Assert(first != end); + first++; + if (first == buf.size()) first = 0; + } void insert(T elem) { // INVARIANT: buf[end] is always unused buf[end++] = elem; if (end == buf.size()) end = 0; diff --git a/src/prop/bvminisat/mtl/Vec.h b/src/prop/bvminisat/mtl/Vec.h index 8ee2a827f..a6e3bca4b 100644 --- a/src/prop/bvminisat/mtl/Vec.h +++ b/src/prop/bvminisat/mtl/Vec.h @@ -21,9 +21,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef BVMinisat_Vec_h #define BVMinisat_Vec_h -#include <assert.h> #include <new> +#include "base/check.h" #include "prop/bvminisat/mtl/IntTypes.h" #include "prop/bvminisat/mtl/XAlloc.h" @@ -42,9 +42,13 @@ class vec { int cap; // Don't allow copying (error prone): - vec<T>& operator = (vec<T>& other) { assert(0); return *this; } - vec (vec<T>& other) { assert(0); } - + vec<T>& operator=(vec<T>& other) + { + Assert(0); + return *this; + } + vec(vec<T>& other) { Assert(0); } + // Helpers for calculating next capacity: static inline int imax (int x, int y) { int mask = (y-x) >> (sizeof(int)*8-1); return (x&mask) + (y&(~mask)); } //static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; } @@ -62,8 +66,16 @@ public: // Size operations: int size (void) const { return sz; } - void shrink (int nelems) { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); } - void shrink_ (int nelems) { assert(nelems <= sz); sz -= nelems; } + void shrink(int nelems) + { + Assert(nelems <= sz); + for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); + } + void shrink_(int nelems) + { + Assert(nelems <= sz); + sz -= nelems; + } int capacity (void) const { return cap; } void capacity (int min_cap); void growTo (int size); @@ -73,8 +85,16 @@ public: // Stack interface: void push (void) { if (sz == cap) capacity(sz+1); new (&data[sz]) T(); sz++; } void push (const T& elem) { if (sz == cap) capacity(sz+1); data[sz++] = elem; } - void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; } - void pop (void) { assert(sz > 0); sz--, data[sz].~T(); } + void push_(const T& elem) + { + Assert(sz < cap); + data[sz++] = elem; + } + void pop(void) + { + Assert(sz > 0); + sz--, data[sz].~T(); + } // NOTE: it seems possible that overflow can happen in the 'sz+1' expression of 'push()', but // in fact it can not since it requires that 'cap' is equal to INT_MAX. This in turn can not // happen given the way capacities are calculated (below). Essentially, all capacities are diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc index 9429e4ced..dcf9ba89b 100644 --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -20,6 +20,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/bvminisat/simp/SimpSolver.h" +#include "base/check.h" #include "options/bv_options.h" #include "options/smt_options.h" #include "proof/clause_id.h" @@ -133,7 +134,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) Var v = var(assumptions[i]); // If an assumption has been eliminated, remember it. - assert(!isEliminated(v)); + Assert(!isEliminated(v)); if (!frozen[v]){ // Freeze and store. @@ -166,8 +167,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) bool SimpSolver::addClause_(vec<Lit>& ps, ClauseId& id) { #ifndef NDEBUG - for (int i = 0; i < ps.size(); i++) - assert(!isEliminated(var(ps[i]))); + for (int i = 0; i < ps.size(); i++) Assert(!isEliminated(var(ps[i]))); #endif int nclauses = clauses.size(); @@ -224,8 +224,8 @@ void SimpSolver::removeClause(CRef cr) bool SimpSolver::strengthenClause(CRef cr, Lit l) { Clause& clause = ca[cr]; - assert(decisionLevel() == 0); - assert(use_simplification); + Assert(decisionLevel() == 0); + Assert(use_simplification); // FIX: this is too inefficient but would be nice to have (properly // implemented) if (!find(subsumption_queue, &clause)) @@ -353,24 +353,26 @@ void SimpSolver::gatherTouchedClauses() bool SimpSolver::implied(const vec<Lit>& clause) { - assert(decisionLevel() == 0); + Assert(decisionLevel() == 0); - trail_lim.push(trail.size()); - for (int i = 0; i < clause.size(); i++) - if (value(clause[i]) == l_True) - { - cancelUntil(0); - return false; - } - else if (value(clause[i]) != l_False) - { - assert(value(clause[i]) == l_Undef); - uncheckedEnqueue(~clause[i]); - } + trail_lim.push(trail.size()); + for (int i = 0; i < clause.size(); i++) + { + if (value(clause[i]) == l_True) + { + cancelUntil(0); + return false; + } + else if (value(clause[i]) != l_False) + { + Assert(value(clause[i]) == l_Undef); + uncheckedEnqueue(~clause[i]); + } + } - bool result = propagate() != CRef_Undef; - cancelUntil(0); - return result; + bool result = propagate() != CRef_Undef; + cancelUntil(0); + return result; } @@ -380,7 +382,7 @@ bool SimpSolver::backwardSubsumptionCheck(bool verbose) int cnt = 0; int subsumed = 0; int deleted_literals = 0; - assert(decisionLevel() == 0); + Assert(decisionLevel() == 0); while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){ @@ -405,7 +407,7 @@ bool SimpSolver::backwardSubsumptionCheck(bool verbose) if (verbose && verbosity >= 2 && cnt++ % 1000 == 0) printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals); - assert(clause.size() > 1 + Assert(clause.size() > 1 || value(clause[0]) == l_True); // Unit-clauses should have been // propagated before this point. @@ -450,7 +452,7 @@ bool SimpSolver::backwardSubsumptionCheck(bool verbose) bool SimpSolver::asymm(Var v, CRef cr) { Clause& clause = ca[cr]; - assert(decisionLevel() == 0); + Assert(decisionLevel() == 0); if (clause.mark() || satisfied(clause)) return true; @@ -477,18 +479,16 @@ bool SimpSolver::asymm(Var v, CRef cr) bool SimpSolver::asymmVar(Var v) { - assert(use_simplification); + Assert(use_simplification); - const vec<CRef>& cls = occurs.lookup(v); + const vec<CRef>& cls = occurs.lookup(v); - if (value(v) != l_Undef || cls.size() == 0) - return true; + if (value(v) != l_Undef || cls.size() == 0) return true; - for (int i = 0; i < cls.size(); i++) - if (!asymm(v, cls[i])) - return false; + for (int i = 0; i < cls.size(); i++) + if (!asymm(v, cls[i])) return false; - return backwardSubsumptionCheck(); + return backwardSubsumptionCheck(); } @@ -510,7 +510,7 @@ static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& clause) elimclauses.push(toInt(clause[i])); if (var(clause[i]) == v) v_pos = i + first; } - assert(v_pos != -1); + Assert(v_pos != -1); // Swap the first literal with the 'v' literal, so that the literal // containing 'v' will occur first in the clause: @@ -526,45 +526,48 @@ static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& clause) bool SimpSolver::eliminateVar(Var v) { + Assert(!frozen[v]); + Assert(!isEliminated(v)); + Assert(value(v) == l_Undef); + + // Split the occurrences into positive and negative: + // + const vec<CRef>& cls = occurs.lookup(v); + vec<CRef> pos, neg; + for (int i = 0; i < cls.size(); i++) + (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]); + + // Check whether the increase in number of clauses stays within the allowed + // ('grow'). Moreover, no clause must exceed the limit on the maximal clause + // size (if it is set): + // + int cnt = 0; + int clause_size = 0; + + for (int i = 0; i < pos.size(); i++) + for (int j = 0; j < neg.size(); j++) + if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) + && (++cnt > cls.size() + grow + || (clause_lim != -1 && clause_size > clause_lim))) + return true; - assert(!frozen[v]); - assert(!isEliminated(v)); - assert(value(v) == l_Undef); - - // Split the occurrences into positive and negative: - // - const vec<CRef>& cls = occurs.lookup(v); - vec<CRef> pos, neg; - for (int i = 0; i < cls.size(); i++) - (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]); - - // Check whether the increase in number of clauses stays within the allowed ('grow'). Moreover, no - // clause must exceed the limit on the maximal clause size (if it is set): - // - int cnt = 0; - int clause_size = 0; + // Delete and store old clauses: + eliminated[v] = true; + setDecisionVar(v, false); + eliminated_vars++; + if (pos.size() > neg.size()) + { + for (int i = 0; i < neg.size(); i++) + mkElimClause(elimclauses, v, ca[neg[i]]); + mkElimClause(elimclauses, mkLit(v)); + } + else + { for (int i = 0; i < pos.size(); i++) - for (int j = 0; j < neg.size(); j++) - if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) - && (++cnt > cls.size() + grow - || (clause_lim != -1 && clause_size > clause_lim))) - return true; - - // Delete and store old clauses: - eliminated[v] = true; - setDecisionVar(v, false); - eliminated_vars++; - - if (pos.size() > neg.size()){ - for (int i = 0; i < neg.size(); i++) - mkElimClause(elimclauses, v, ca[neg[i]]); - mkElimClause(elimclauses, mkLit(v)); - }else{ - for (int i = 0; i < pos.size(); i++) - mkElimClause(elimclauses, v, ca[pos[i]]); - mkElimClause(elimclauses, ~mkLit(v)); - } + mkElimClause(elimclauses, v, ca[pos[i]]); + mkElimClause(elimclauses, ~mkLit(v)); + } for (int i = 0; i < cls.size(); i++) removeClause(cls[i]); @@ -591,33 +594,33 @@ bool SimpSolver::eliminateVar(Var v) bool SimpSolver::substitute(Var v, Lit x) { - assert(!frozen[v]); - assert(!isEliminated(v)); - assert(value(v) == l_Undef); - - if (!ok) return false; + Assert(!frozen[v]); + Assert(!isEliminated(v)); + Assert(value(v) == l_Undef); - eliminated[v] = true; - setDecisionVar(v, false); - const vec<CRef>& cls = occurs.lookup(v); + if (!ok) return false; - vec<Lit>& subst_clause = add_tmp; - for (int i = 0; i < cls.size(); i++){ - Clause& clause = ca[cls[i]]; + eliminated[v] = true; + setDecisionVar(v, false); + const vec<CRef>& cls = occurs.lookup(v); - subst_clause.clear(); - for (int j = 0; j < clause.size(); j++) - { - Lit p = clause[j]; - subst_clause.push(var(p) == v ? x ^ sign(p) : p); - } + vec<Lit>& subst_clause = add_tmp; + for (int i = 0; i < cls.size(); i++) + { + Clause& clause = ca[cls[i]]; - removeClause(cls[i]); - ClauseId id; - if (!addClause_(subst_clause, id)) - return ok = false; + subst_clause.clear(); + for (int j = 0; j < clause.size(); j++) + { + Lit p = clause[j]; + subst_clause.push(var(p) == v ? x ^ sign(p) : p); } + removeClause(cls[i]); + ClauseId id; + if (!addClause_(subst_clause, id)) return ok = false; + } + return true; } @@ -664,11 +667,12 @@ bool SimpSolver::eliminate(bool turn_off_elim) // Empty elim_heap and return immediately on user-interrupt: if (asynch_interrupt){ - assert(bwdsub_assigns == trail.size()); - assert(subsumption_queue.size() == 0); - assert(n_touched == 0); - elim_heap.clear(); - goto cleanup; } + Assert(bwdsub_assigns == trail.size()); + Assert(subsumption_queue.size() == 0); + Assert(n_touched == 0); + elim_heap.clear(); + goto cleanup; + } // printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size()); for (int cnt = 0; !elim_heap.empty(); cnt++){ @@ -697,7 +701,7 @@ bool SimpSolver::eliminate(bool turn_off_elim) checkGarbage(simp_garbage_frac); } - assert(subsumption_queue.size() == 0); + Assert(subsumption_queue.size() == 0); } cleanup: diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index c76878da4..bf23a7dff 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -21,6 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef BVMinisat_SimpSolver_h #define BVMinisat_SimpSolver_h +#include "base/check.h" #include "proof/clause_id.h" #include "prop/bvminisat/core/Solver.h" #include "prop/bvminisat/mtl/Queue.h" @@ -188,11 +189,12 @@ class SimpSolver : public Solver { inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v]; } inline void SimpSolver::updateElimHeap(Var v) { - assert(use_simplification); - // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef) - if (elim_heap.inHeap(v) || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)) - elim_heap.update(v); } - + Assert(use_simplification); + // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef) + if (elim_heap.inHeap(v) + || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)) + elim_heap.update(v); +} inline bool SimpSolver::addClause (const vec<Lit>& ps, ClauseId& id) { ps.copyTo(add_tmp); return addClause_(add_tmp, id); } inline bool SimpSolver::addEmptyClause() { add_tmp.clear(); ClauseId id; return addClause_(add_tmp, id); } diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index d597ac934..b36fe9517 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -25,6 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <iostream> #include <unordered_set> +#include "base/check.h" #include "base/output.h" #include "options/main_options.h" #include "options/prop_options.h" @@ -292,8 +293,8 @@ Var Solver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister, bo } void Solver::resizeVars(int newSize) { - assert(d_enable_incremental); - assert(decisionLevel() == 0); + Assert(d_enable_incremental); + Assert(decisionLevel() == 0); Assert(newSize >= 2) << "always keep true/false"; if (newSize < nVars()) { int shrinkSize = nVars() - newSize; @@ -313,7 +314,7 @@ void Solver::resizeVars(int newSize) { if (Debug.isOn("minisat::pop")) { for (int i = 0; i < trail.size(); ++ i) { - assert(var(trail[i]) < nVars()); + Assert(var(trail[i]) < nVars()); } } } @@ -523,7 +524,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) id = ClauseIdUndef; } } else { - assert(decisionLevel() == 0); + Assert(decisionLevel() == 0); // If all false, we're in conflict if (ps.size() == falseLiteralsCount) { @@ -608,7 +609,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) // Check if it propagates if (ps.size() == falseLiteralsCount + 1) { if(assigns[var(ps[0])] == l_Undef) { - assert(assigns[var(ps[0])] != l_False); + Assert(assigns[var(ps[0])] != l_False); uncheckedEnqueue(ps[0], cr); Debug("cores") << "i'm registering a unit clause, maybe input" << std::endl; @@ -714,7 +715,7 @@ void Solver::detachClause(CRef cr, bool strict) { Debug("minisat") << "\n"; } - assert(c.size() > 1); + Assert(c.size() > 1); if (options::unsatCores() && !isProofEnabled()) { ProofManager::getSatProof()->markDeleted(cr); @@ -1006,18 +1007,18 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) d_pfManager->startResChain(ca[confl]); } do{ - assert(confl != CRef_Undef); // (otherwise should be UIP) + Assert(confl != CRef_Undef); // (otherwise should be UIP) - { - // ! IMPORTANT ! - // It is not safe to use c after this block of code because - // resolveOutUnit() below may lead to clauses being allocated, which - // in turn may lead to reallocations that invalidate c. - Clause& c = ca[confl]; - max_resolution_level = std::max(max_resolution_level, c.level()); - - if (c.removable()) claBumpActivity(c); - } + { + // ! IMPORTANT ! + // It is not safe to use c after this block of code because + // resolveOutUnit() below may lead to clauses being allocated, which + // in turn may lead to reallocations that invalidate c. + Clause& c = ca[confl]; + max_resolution_level = std::max(max_resolution_level, c.level()); + + if (c.removable()) claBumpActivity(c); + } if (Trace.isOn("pf::sat")) { @@ -1196,7 +1197,7 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels) int top = analyze_toclear.size(); while (analyze_stack.size() > 0){ CRef c_reason = reason(var(analyze_stack.last())); - assert(c_reason != CRef_Undef); + Assert(c_reason != CRef_Undef); Clause& c = ca[c_reason]; int c_size = c.size(); analyze_stack.pop(); @@ -1252,8 +1253,8 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) Var x = var(trail[i]); if (seen[x]){ if (reason(x) == CRef_Undef){ - assert(level(x) > 0); - out_conflict.push(~trail[i]); + Assert(level(x) > 0); + out_conflict.push(~trail[i]); }else{ Clause& c = ca[reason(x)]; for (int j = 1; j < c.size(); j++) @@ -1292,8 +1293,8 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) } Debug("minisat") << "\n"; } - assert(value(p) == l_Undef); - assert(var(p) < nVars()); + Assert(value(p) == l_Undef); + Assert(var(p) < nVars()); assigns[var(p)] = lbool(!sign(p)); vardata[var(p)] = VarData( from, decisionLevel(), assertionLevel, intro_level(var(p)), trail.size()); @@ -1484,7 +1485,7 @@ CRef Solver::propagateBool() Lit false_lit = ~p; if (c[0] == false_lit) c[0] = c[1], c[1] = false_lit; - assert(c[1] == false_lit); + Assert(c[1] == false_lit); i++; // If 0th watch is true, then clause is already satisfied. @@ -1584,8 +1585,8 @@ void Solver::removeClausesAboveLevel(vec<CRef>& cs, int level) for (i = j = 0; i < cs.size(); i++){ Clause& c = ca[cs[i]]; if (c.level() > level) { - assert(!locked(c)); - removeClause(cs[i]); + Assert(!locked(c)); + removeClause(cs[i]); } else { cs[j++] = cs[i]; } @@ -1613,25 +1614,25 @@ void Solver::rebuildOrderHeap() |________________________________________________________________________________________________@*/ bool Solver::simplify() { - assert(decisionLevel() == 0); + Assert(decisionLevel() == 0); - if (!ok || propagate(CHECK_WITHOUT_THEORY) != CRef_Undef) - return ok = false; + if (!ok || propagate(CHECK_WITHOUT_THEORY) != CRef_Undef) return ok = false; - if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) - return true; + if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) return true; - // Remove satisfied clauses: - removeSatisfied(clauses_removable); - if (remove_satisfied) // Can be turned off. - removeSatisfied(clauses_persistent); - checkGarbage(); - rebuildOrderHeap(); + // Remove satisfied clauses: + removeSatisfied(clauses_removable); + if (remove_satisfied) // Can be turned off. + removeSatisfied(clauses_persistent); + checkGarbage(); + rebuildOrderHeap(); - simpDB_assigns = nAssigns(); - simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now) + simpDB_assigns = nAssigns(); + simpDB_props = + clauses_literals + learnts_literals; // (shouldn't depend on stats + // really, but it will do for now) - return true; + return true; } @@ -1650,186 +1651,209 @@ bool Solver::simplify() |________________________________________________________________________________________________@*/ lbool Solver::search(int nof_conflicts) { - assert(ok); - int backtrack_level; - int conflictC = 0; - vec<Lit> learnt_clause; - starts++; - - TheoryCheckType check_type = CHECK_WITH_THEORY; - for (;;) { - - // Propagate and call the theory solvers - CRef confl = propagate(check_type); - Assert(lemmas.size() == 0); - - if (confl != CRef_Undef) { + Assert(ok); + int backtrack_level; + int conflictC = 0; + vec<Lit> learnt_clause; + starts++; + + TheoryCheckType check_type = CHECK_WITH_THEORY; + for (;;) + { + // Propagate and call the theory solvers + CRef confl = propagate(check_type); + Assert(lemmas.size() == 0); - conflicts++; conflictC++; + if (confl != CRef_Undef) + { + conflicts++; + conflictC++; - if (decisionLevel() == 0) - { - if (options::unsatCores() && !isProofEnabled()) - { - ProofManager::getSatProof()->finalizeProof(confl); - } - if (isProofEnabled()) - { - if (confl == CRef_Lazy) - { - d_pfManager->finalizeProof(); - } - else - { - d_pfManager->finalizeProof(ca[confl]); - } - } - return l_False; - } + if (decisionLevel() == 0) + { + if (options::unsatCores() && !isProofEnabled()) + { + ProofManager::getSatProof()->finalizeProof(confl); + } + if (isProofEnabled()) + { + if (confl == CRef_Lazy) + { + d_pfManager->finalizeProof(); + } + else + { + d_pfManager->finalizeProof(ca[confl]); + } + } + return l_False; + } - // Analyze the conflict - learnt_clause.clear(); - int max_level = analyze(confl, learnt_clause, backtrack_level); - cancelUntil(backtrack_level); + // Analyze the conflict + learnt_clause.clear(); + int max_level = analyze(confl, learnt_clause, backtrack_level); + cancelUntil(backtrack_level); - // Assert the conflict clause and the asserting literal - if (learnt_clause.size() == 1) { - uncheckedEnqueue(learnt_clause[0]); - if (options::unsatCores() && !isProofEnabled()) - { - ProofManager::getSatProof()->endResChain(learnt_clause[0]); - } - if (isProofEnabled()) - { - d_pfManager->endResChain(learnt_clause[0]); - } - } else { - CRef cr = - ca.alloc(assertionLevelOnly() ? assertionLevel : max_level, + // Assert the conflict clause and the asserting literal + if (learnt_clause.size() == 1) + { + uncheckedEnqueue(learnt_clause[0]); + if (options::unsatCores() && !isProofEnabled()) + { + ProofManager::getSatProof()->endResChain(learnt_clause[0]); + } + if (isProofEnabled()) + { + d_pfManager->endResChain(learnt_clause[0]); + } + } + else + { + CRef cr = ca.alloc(assertionLevelOnly() ? assertionLevel : max_level, learnt_clause, true); - clauses_removable.push(cr); - attachClause(cr); - claBumpActivity(ca[cr]); - uncheckedEnqueue(learnt_clause[0], cr); - if (options::unsatCores() && !isProofEnabled()) - { - ClauseId id = - ProofManager::getSatProof()->registerClause(cr, LEARNT); - ProofManager::getSatProof()->endResChain(id); - } - if (isProofEnabled()) - { - d_pfManager->endResChain(ca[cr]); - } - } - - varDecayActivity(); - claDecayActivity(); - - if (--learntsize_adjust_cnt == 0){ - learntsize_adjust_confl *= learntsize_adjust_inc; - learntsize_adjust_cnt = (int)learntsize_adjust_confl; - max_learnts *= learntsize_inc; - - if (verbosity >= 1) - printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", - (int)conflicts, - (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals, - (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100); - } + clauses_removable.push(cr); + attachClause(cr); + claBumpActivity(ca[cr]); + uncheckedEnqueue(learnt_clause[0], cr); + if (options::unsatCores() && !isProofEnabled()) + { + ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT); + ProofManager::getSatProof()->endResChain(id); + } + if (isProofEnabled()) + { + d_pfManager->endResChain(ca[cr]); + } + } - if (theoryConflict && options::sat_refine_conflicts()) { - check_type = CHECK_FINAL_FAKE; - } else { - check_type = CHECK_WITH_THEORY; - } + varDecayActivity(); + claDecayActivity(); - } else { - // If this was a final check, we are satisfiable - if (check_type == CHECK_FINAL) - { - bool decisionEngineDone = d_proxy->isDecisionEngineDone(); - // Unless a lemma has added more stuff to the queues - if (!decisionEngineDone - && (!order_heap.empty() || qhead < trail.size())) - { - check_type = CHECK_WITH_THEORY; - continue; - } - else if (recheck) - { - // There some additional stuff added, so we go for another - // full-check - continue; - } - else - { - // Yes, we're truly satisfiable - return l_True; - } - } - else if (check_type == CHECK_FINAL_FAKE) - { - check_type = CHECK_WITH_THEORY; - } + if (--learntsize_adjust_cnt == 0) + { + learntsize_adjust_confl *= learntsize_adjust_inc; + learntsize_adjust_cnt = (int)learntsize_adjust_confl; + max_learnts *= learntsize_inc; + + if (verbosity >= 1) + printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", + (int)conflicts, + (int)dec_vars + - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), + nClauses(), + (int)clauses_literals, + (int)max_learnts, + nLearnts(), + (double)learnts_literals / nLearnts(), + progressEstimate() * 100); + } - if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) - || !withinBudget(ResourceManager::Resource::SatConflictStep)) - { - // Reached bound on number of conflicts: - progress_estimate = progressEstimate(); - cancelUntil(0); - // [mdeters] notify theory engine of restarts for deferred - // theory processing - d_proxy->notifyRestart(); - return l_Undef; - } + if (theoryConflict && options::sat_refine_conflicts()) + { + check_type = CHECK_FINAL_FAKE; + } + else + { + check_type = CHECK_WITH_THEORY; + } + } + else + { + // If this was a final check, we are satisfiable + if (check_type == CHECK_FINAL) + { + bool decisionEngineDone = d_proxy->isDecisionEngineDone(); + // Unless a lemma has added more stuff to the queues + if (!decisionEngineDone + && (!order_heap.empty() || qhead < trail.size())) + { + check_type = CHECK_WITH_THEORY; + continue; + } + else if (recheck) + { + // There some additional stuff added, so we go for another + // full-check + continue; + } + else + { + // Yes, we're truly satisfiable + return l_True; + } + } + else if (check_type == CHECK_FINAL_FAKE) + { + check_type = CHECK_WITH_THEORY; + } - // Simplify the set of problem clauses: - if (decisionLevel() == 0 && !simplify()) { - return l_False; - } + if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) + || !withinBudget(ResourceManager::Resource::SatConflictStep)) + { + // Reached bound on number of conflicts: + progress_estimate = progressEstimate(); + cancelUntil(0); + // [mdeters] notify theory engine of restarts for deferred + // theory processing + d_proxy->notifyRestart(); + return l_Undef; + } - if (clauses_removable.size()-nAssigns() >= max_learnts) { - // Reduce the set of learnt clauses: - reduceDB(); - } + // Simplify the set of problem clauses: + if (decisionLevel() == 0 && !simplify()) + { + return l_False; + } - Lit next = lit_Undef; - while (decisionLevel() < assumptions.size()) { - // Perform user provided assumption: - Lit p = assumptions[decisionLevel()]; - if (value(p) == l_True) { - // Dummy decision level: - newDecisionLevel(); - } else if (value(p) == l_False) { - analyzeFinal(~p, d_conflict); - return l_False; - } else { - next = p; - break; - } - } + if (clauses_removable.size() - nAssigns() >= max_learnts) + { + // Reduce the set of learnt clauses: + reduceDB(); + } - if (next == lit_Undef) { - // New variable decision: - next = pickBranchLit(); + Lit next = lit_Undef; + while (decisionLevel() < assumptions.size()) + { + // Perform user provided assumption: + Lit p = assumptions[decisionLevel()]; + if (value(p) == l_True) + { + // Dummy decision level: + newDecisionLevel(); + } + else if (value(p) == l_False) + { + analyzeFinal(~p, d_conflict); + return l_False; + } + else + { + next = p; + break; + } + } - if (next == lit_Undef) { - // We need to do a full theory check to confirm - Debug("minisat::search") << "Doing a full theory check..." - << std::endl; - check_type = CHECK_FINAL; - continue; - } - } + if (next == lit_Undef) + { + // New variable decision: + next = pickBranchLit(); - // Increase decision level and enqueue 'next' - newDecisionLevel(); - uncheckedEnqueue(next); + if (next == lit_Undef) + { + // We need to do a full theory check to confirm + Debug("minisat::search") + << "Doing a full theory check..." << std::endl; + check_type = CHECK_FINAL; + continue; } + } + + // Increase decision level and enqueue 'next' + newDecisionLevel(); + uncheckedEnqueue(next); } + } } @@ -1882,7 +1906,7 @@ lbool Solver::solve_() ScopedBool scoped_bool(minisat_busy, true); - assert(decisionLevel() == 0); + Assert(decisionLevel() == 0); model.clear(); d_conflict.clear(); @@ -2002,8 +2026,11 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps) fprintf(f, "p cnf %d %d\n", max, cnt); for (int i = 0; i < assumptions.size(); i++){ - assert(value(assumptions[i]) != l_False); - fprintf(f, "%s%d 0\n", sign(assumptions[i]) ? "-" : "", mapVar(var(assumptions[i]), map, max)+1); + Assert(value(assumptions[i]) != l_False); + fprintf(f, + "%s%d 0\n", + sign(assumptions[i]) ? "-" : "", + mapVar(var(assumptions[i]), map, max) + 1); } for (int i = 0; i < clauses_persistent.size(); i++) @@ -2095,8 +2122,8 @@ void Solver::garbageCollect() void Solver::push() { - assert(d_enable_incremental); - assert(decisionLevel() == 0); + Assert(d_enable_incremental); + Assert(decisionLevel() == 0); ++assertionLevel; Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl; @@ -2110,9 +2137,9 @@ void Solver::push() void Solver::pop() { - assert(d_enable_incremental); + Assert(d_enable_incremental); - assert(decisionLevel() == 0); + Assert(decisionLevel() == 0); // Pop the trail below the user level --assertionLevel; diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index f685017a7..b3ed72a4c 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -21,12 +21,12 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_Solver_h #define Minisat_Solver_h -#include "cvc4_private.h" - #include <iosfwd> +#include "base/check.h" #include "base/output.h" #include "context/context.h" +#include "cvc4_private.h" #include "expr/proof_node_manager.h" #include "proof/clause_id.h" #include "prop/minisat/core/SolverTypes.h" @@ -534,31 +534,32 @@ inline bool Solver::isDecision(Var x) const inline int Solver::level(Var x) const { - assert(x < vardata.size()); + Assert(x < vardata.size()); return vardata[x].d_level; } inline int Solver::user_level(Var x) const { - assert(x < vardata.size()); + Assert(x < vardata.size()); return vardata[x].d_user_level; } inline int Solver::intro_level(Var x) const { - assert(x < vardata.size()); + Assert(x < vardata.size()); return vardata[x].d_intro_level; } inline int Solver::trail_index(Var x) const { - assert(x < vardata.size()); + Assert(x < vardata.size()); return vardata[x].d_trail_index; } inline void Solver::insertVarOrder(Var x) { - assert(x < vardata.size()); - if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); } + Assert(x < vardata.size()); + if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); +} inline void Solver::varDecayActivity() { var_inc *= (1 / var_decay); } inline void Solver::varBumpActivity(Var v) { varBumpActivity(v, var_inc); } @@ -607,8 +608,16 @@ inline void Solver::newDecisionLevel() inline int Solver::decisionLevel () const { return trail_lim.size(); } inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); } -inline lbool Solver::value (Var x) const { assert(x < nVars()); return assigns[x]; } -inline lbool Solver::value (Lit p) const { assert(var(p) < nVars()); return assigns[var(p)] ^ sign(p); } +inline lbool Solver::value(Var x) const +{ + Assert(x < nVars()); + return assigns[x]; +} +inline lbool Solver::value(Lit p) const +{ + Assert(var(p) < nVars()); + return assigns[var(p)] ^ sign(p); +} inline lbool Solver::modelValue (Var x) const { return model[x]; } inline lbool Solver::modelValue (Lit p) const { return model[var(p)] ^ sign(p); } inline int Solver::nAssigns () const { return trail.size(); } diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index b30d97aee..f2d2860c8 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -23,13 +23,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_SolverTypes_h #define Minisat_SolverTypes_h -#include <assert.h> +#include "base/check.h" #include "base/output.h" -#include "prop/minisat/mtl/IntTypes.h" #include "prop/minisat/mtl/Alg.h" -#include "prop/minisat/mtl/Vec.h" -#include "prop/minisat/mtl/Map.h" #include "prop/minisat/mtl/Alloc.h" +#include "prop/minisat/mtl/IntTypes.h" +#include "prop/minisat/mtl/Map.h" +#include "prop/minisat/mtl/Vec.h" namespace CVC4 { namespace Minisat { @@ -226,16 +226,21 @@ class Clause { public: void calcAbstraction() { - assert(header.has_extra); - uint32_t abstraction = 0; - for (int i = 0; i < size(); i++) - abstraction |= 1 << (var(data[i].lit) & 31); - data[header.size].abs = abstraction; } - + Assert(header.has_extra); + uint32_t abstraction = 0; + for (int i = 0; i < size(); i++) + abstraction |= 1 << (var(data[i].lit) & 31); + data[header.size].abs = abstraction; + } int level () const { return header.level; } int size () const { return header.size; } - void shrink (int i) { assert(i <= size()); if (header.has_extra) data[header.size-i] = data[header.size]; header.size -= i; } + void shrink(int i) + { + Assert(i <= size()); + if (header.has_extra) data[header.size - i] = data[header.size]; + header.size -= i; + } void pop () { shrink(1); } bool removable () const { return header.removable; } bool has_extra () const { return header.has_extra; } @@ -253,8 +258,16 @@ public: Lit operator [] (int i) const { return data[i].lit; } operator const Lit* (void) const { return (Lit*)data; } - float& activity () { assert(header.has_extra); return data[header.size].act; } - uint32_t abstraction () const { assert(header.has_extra); return data[header.size].abs; } + float& activity() + { + Assert(header.has_extra); + return data[header.size].act; + } + uint32_t abstraction() const + { + Assert(header.has_extra); + return data[header.size].abs; + } Lit subsumes (const Clause& other) const; void strengthen (Lit p); @@ -284,14 +297,15 @@ class ClauseAllocator : public RegionAllocator<uint32_t> template<class Lits> CRef alloc(int level, const Lits& ps, bool removable = false) { - assert(sizeof(Lit) == sizeof(uint32_t)); - assert(sizeof(float) == sizeof(uint32_t)); - bool use_extra = removable | extra_clause_field; + Assert(sizeof(Lit) == sizeof(uint32_t)); + Assert(sizeof(float) == sizeof(uint32_t)); + bool use_extra = removable | extra_clause_field; - CRef cid = RegionAllocator<uint32_t>::alloc(clauseWord32Size(ps.size(), use_extra)); - new (lea(cid)) Clause(ps, use_extra, removable, level); + CRef cid = RegionAllocator<uint32_t>::alloc( + clauseWord32Size(ps.size(), use_extra)); + new (lea(cid)) Clause(ps, use_extra, removable, level); - return cid; + return cid; } // Deref, Load Effective Address (LEA), Inverse of LEA (AEL): @@ -450,8 +464,10 @@ inline Lit Clause::subsumes(const Clause& other) const //if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0) //if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0)) - assert(!header.removable); assert(!other.header.removable); - assert(header.has_extra); assert(other.header.has_extra); + Assert(!header.removable); + Assert(!other.header.removable); + Assert(header.has_extra); + Assert(other.header.has_extra); if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0) return lit_Error; diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h index 365b2d5aa..2f8a86c3b 100644 --- a/src/prop/minisat/mtl/Alg.h +++ b/src/prop/minisat/mtl/Alg.h @@ -21,6 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_Alg_h #define Minisat_Alg_h +#include "base/check.h" #include "prop/minisat/mtl/Vec.h" namespace CVC4 { @@ -38,7 +39,7 @@ static inline void remove(V& ts, const T& t) { int j = 0; for (; j < ts.size() && ts[j] != t; j++); - assert(j < ts.size()); + Assert(j < ts.size()); for (; j < ts.size()-1; j++) ts[j] = ts[j+1]; ts.pop(); } diff --git a/src/prop/minisat/mtl/Alloc.h b/src/prop/minisat/mtl/Alloc.h index e5b171bac..98e59e7bf 100644 --- a/src/prop/minisat/mtl/Alloc.h +++ b/src/prop/minisat/mtl/Alloc.h @@ -21,8 +21,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_Alloc_h #define Minisat_Alloc_h -#include "prop/minisat/mtl/XAlloc.h" +#include "base/check.h" #include "prop/minisat/mtl/Vec.h" +#include "prop/minisat/mtl/XAlloc.h" namespace CVC4 { namespace Minisat { @@ -61,13 +62,33 @@ class RegionAllocator void free (int size) { wasted_ += size; } // Deref, Load Effective Address (LEA), Inverse of LEA (AEL): - T& operator[](Ref r) { assert(r >= 0 && r < sz); return memory[r]; } - const T& operator[](Ref r) const { assert(r >= 0 && r < sz); return memory[r]; } + T& operator[](Ref r) + { + Assert(r >= 0 && r < sz); + return memory[r]; + } + const T& operator[](Ref r) const + { + Assert(r >= 0 && r < sz); + return memory[r]; + } - T* lea (Ref r) { assert(r >= 0 && r < sz); return &memory[r]; } - const T* lea (Ref r) const { assert(r >= 0 && r < sz); return &memory[r]; } - Ref ael (const T* t) { assert((void*)t >= (void*)&memory[0] && (void*)t < (void*)&memory[sz-1]); - return (Ref)(t - &memory[0]); } + T* lea(Ref r) + { + Assert(r >= 0 && r < sz); + return &memory[r]; + } + const T* lea(Ref r) const + { + Assert(r >= 0 && r < sz); + return &memory[r]; + } + Ref ael(const T* t) + { + Assert((void*)t >= (void*)&memory[0] + && (void*)t < (void*)&memory[sz - 1]); + return (Ref)(t - &memory[0]); + } void moveTo(RegionAllocator& to) { if (to.memory != NULL) ::free(to.memory); @@ -102,7 +123,7 @@ void RegionAllocator<T>::capacity(uint32_t min_cap) } // printf(" .. (%p) cap = %u\n", this, cap); - assert(cap > 0); + Assert(cap > 0); memory = (T*)xrealloc(memory, sizeof(T)*cap); } @@ -112,7 +133,7 @@ typename RegionAllocator<T>::Ref RegionAllocator<T>::alloc(int size) { // printf("ALLOC called (this = %p, size = %d)\n", this, size); fflush(stdout); - assert(size > 0); + Assert(size > 0); capacity(sz + size); uint32_t prev_sz = sz; diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h index c990f9a99..1e64f6ba5 100644 --- a/src/prop/minisat/mtl/Heap.h +++ b/src/prop/minisat/mtl/Heap.h @@ -21,6 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_Heap_h #define Minisat_Heap_h +#include "base/check.h" #include "prop/minisat/mtl/Vec.h" namespace CVC4 { @@ -79,12 +80,22 @@ class Heap { int size () const { return heap.size(); } bool empty () const { return heap.size() == 0; } bool inHeap (int n) const { return n < indices.size() && indices[n] >= 0; } - int operator[](int index) const { assert(index < heap.size()); return heap[index]; } - - - void decrease (int n) { assert(inHeap(n)); percolateUp (indices[n]); } - void increase (int n) { assert(inHeap(n)); percolateDown(indices[n]); } + int operator[](int index) const + { + Assert(index < heap.size()); + return heap[index]; + } + void decrease(int n) + { + Assert(inHeap(n)); + percolateUp(indices[n]); + } + void increase(int n) + { + Assert(inHeap(n)); + percolateDown(indices[n]); + } // Safe variant of insert/decrease/increase: void update(int n) @@ -100,7 +111,7 @@ class Heap { void insert(int n) { indices.growTo(n+1, -1); - assert(!inHeap(n)); + Assert(!inHeap(n)); indices[n] = heap.size(); heap.push(n); diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h index 17572713f..bf299d55d 100644 --- a/src/prop/minisat/mtl/Map.h +++ b/src/prop/minisat/mtl/Map.h @@ -20,6 +20,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_Map_h #define Minisat_Map_h +#include "base/check.h" #include "prop/minisat/mtl/IntTypes.h" #include "prop/minisat/mtl/Vec.h" @@ -68,8 +69,8 @@ class Map { int size; // Don't allow copying (error prone): - Map<K,D,H,E>& operator = (Map<K,D,H,E>& other) { assert(0); } - Map (Map<K,D,H,E>& other) { assert(0); } + Map<K, D, H, E>& operator=(Map<K, D, H, E>& other) { Assert(0); } + Map(Map<K, D, H, E>& other) { Assert(0); } bool checkCap(int new_size) const { return new_size > cap; } @@ -108,27 +109,25 @@ class Map { // PRECONDITION: the key must already exist in the map. const D& operator [] (const K& k) const { - assert(size != 0); - const D* res = NULL; - const vec<Pair>& ps = table[index(k)]; - for (int i = 0; i < ps.size(); i++) - if (equals(ps[i].key, k)) - res = &ps[i].data; - assert(res != NULL); - return *res; + Assert(size != 0); + const D* res = NULL; + const vec<Pair>& ps = table[index(k)]; + for (int i = 0; i < ps.size(); i++) + if (equals(ps[i].key, k)) res = &ps[i].data; + Assert(res != NULL); + return *res; } // PRECONDITION: the key must already exist in the map. D& operator [] (const K& k) { - assert(size != 0); - D* res = NULL; - vec<Pair>& ps = table[index(k)]; - for (int i = 0; i < ps.size(); i++) - if (equals(ps[i].key, k)) - res = &ps[i].data; - assert(res != NULL); - return *res; + Assert(size != 0); + D* res = NULL; + vec<Pair>& ps = table[index(k)]; + for (int i = 0; i < ps.size(); i++) + if (equals(ps[i].key, k)) res = &ps[i].data; + Assert(res != NULL); + return *res; } // PRECONDITION: the key must *NOT* exist in the map. @@ -154,14 +153,15 @@ class Map { // PRECONDITION: the key must exist in the map. void remove(const K& k) { - assert(table != NULL); - vec<Pair>& ps = table[index(k)]; - int j = 0; - for (; j < ps.size() && !equals(ps[j].key, k); j++); - assert(j < ps.size()); - ps[j] = ps.last(); - ps.pop(); - size--; + Assert(table != NULL); + vec<Pair>& ps = table[index(k)]; + int j = 0; + for (; j < ps.size() && !equals(ps[j].key, k); j++) + ; + Assert(j < ps.size()); + ps[j] = ps.last(); + ps.pop(); + size--; } void clear () { diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h index ca2014429..242bc9388 100644 --- a/src/prop/minisat/mtl/Queue.h +++ b/src/prop/minisat/mtl/Queue.h @@ -21,6 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_Queue_h #define Minisat_Queue_h +#include "base/check.h" #include "prop/minisat/mtl/Vec.h" namespace CVC4 { @@ -42,11 +43,30 @@ public: void clear (bool dealloc = false) { buf.clear(dealloc); buf.growTo(1); first = end = 0; } int size () const { return (end >= first) ? end - first : end - first + buf.size(); } - const T& operator [] (int index) const { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; } - T& operator [] (int index) { assert(index >= 0); assert(index < size()); return buf[(first + index) % buf.size()]; } + const T& operator[](int index) const + { + Assert(index >= 0); + Assert(index < size()); + return buf[(first + index) % buf.size()]; + } + T& operator[](int index) + { + Assert(index >= 0); + Assert(index < size()); + return buf[(first + index) % buf.size()]; + } - T peek () const { assert(first != end); return buf[first]; } - void pop () { assert(first != end); first++; if (first == buf.size()) first = 0; } + T peek() const + { + Assert(first != end); + return buf[first]; + } + void pop() + { + Assert(first != end); + first++; + if (first == buf.size()) first = 0; + } void insert(T elem) { // INVARIANT: buf[end] is always unused buf[end++] = elem; if (end == buf.size()) end = 0; diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h index cb81ee580..08e40e8bc 100644 --- a/src/prop/minisat/mtl/Vec.h +++ b/src/prop/minisat/mtl/Vec.h @@ -21,9 +21,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_Vec_h #define Minisat_Vec_h -#include <assert.h> #include <new> +#include "base/check.h" #include "prop/minisat/mtl/IntTypes.h" #include "prop/minisat/mtl/XAlloc.h" @@ -42,9 +42,13 @@ class vec { int cap; // Don't allow copying (error prone): - vec<T>& operator = (vec<T>& other) { assert(0); return *this; } - vec (vec<T>& other) { assert(0); } - + vec<T>& operator=(vec<T>& other) + { + Assert(0); + return *this; + } + vec(vec<T>& other) { Assert(0); } + // Helpers for calculating next capacity: static inline int imax (int x, int y) { int mask = (y-x) >> (sizeof(int)*8-1); return (x&mask) + (y&(~mask)); } //static inline void nextCap(int& cap){ cap += ((cap >> 1) + 2) & ~1; } @@ -62,8 +66,16 @@ public: // Size operations: int size (void) const { return sz; } - void shrink (int nelems) { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); } - void shrink_ (int nelems) { assert(nelems <= sz); sz -= nelems; } + void shrink(int nelems) + { + Assert(nelems <= sz); + for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); + } + void shrink_(int nelems) + { + Assert(nelems <= sz); + sz -= nelems; + } int capacity (void) const { return cap; } void capacity (int min_cap); void growTo (int size); @@ -73,8 +85,16 @@ public: // Stack interface: void push (void) { if (sz == cap) capacity(sz+1); new (&data[sz]) T(); sz++; } void push (const T& elem) { if (sz == cap) capacity(sz+1); data[sz++] = elem; } - void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; } - void pop (void) { assert(sz > 0); sz--, data[sz].~T(); } + void push_(const T& elem) + { + Assert(sz < cap); + data[sz++] = elem; + } + void pop(void) + { + Assert(sz > 0); + sz--, data[sz].~T(); + } // NOTE: it seems possible that overflow can happen in the 'sz+1' expression of 'push()', but // in fact it can not since it requires that 'cap' is equal to INT_MAX. This in turn can not // happen given the way capacities are calculated (below). Essentially, all capacities are diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc index 4649a67aa..e925bad09 100644 --- a/src/prop/minisat/simp/SimpSolver.cc +++ b/src/prop/minisat/simp/SimpSolver.cc @@ -20,6 +20,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/simp/SimpSolver.h" +#include "base/check.h" #include "options/prop_options.h" #include "options/smt_options.h" #include "proof/clause_id.h" @@ -127,7 +128,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) toDimacs(); return l_Undef; } - assert(decisionLevel() == 0); + Assert(decisionLevel() == 0); vec<Var> extra_frozen; lbool result = l_True; @@ -140,7 +141,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) Var v = var(assumptions[i]); // If an assumption has been eliminated, remember it. - assert(!isEliminated(v)); + Assert(!isEliminated(v)); if (!frozen[v]){ // Freeze and store. @@ -173,8 +174,7 @@ bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) { #ifndef NDEBUG if (use_simplification) { - for (int i = 0; i < ps.size(); i++) - assert(!isEliminated(var(ps[i]))); + for (int i = 0; i < ps.size(); i++) Assert(!isEliminated(var(ps[i]))); } #endif @@ -230,8 +230,8 @@ void SimpSolver::removeClause(CRef cr) bool SimpSolver::strengthenClause(CRef cr, Lit l) { Clause& c = ca[cr]; - assert(decisionLevel() == 0); - assert(use_simplification); + Assert(decisionLevel() == 0); + Assert(use_simplification); // FIX: this is too inefficient but would be nice to have (properly implemented) // if (!find(subsumption_queue, &c)) @@ -356,21 +356,26 @@ void SimpSolver::gatherTouchedClauses() bool SimpSolver::implied(const vec<Lit>& c) { - assert(decisionLevel() == 0); + Assert(decisionLevel() == 0); - trail_lim.push(trail.size()); - for (int i = 0; i < c.size(); i++) - if (value(c[i]) == l_True){ - cancelUntil(0); - return false; - }else if (value(c[i]) != l_False){ - assert(value(c[i]) == l_Undef); - uncheckedEnqueue(~c[i]); - } + trail_lim.push(trail.size()); + for (int i = 0; i < c.size(); i++) + { + if (value(c[i]) == l_True) + { + cancelUntil(0); + return false; + } + else if (value(c[i]) != l_False) + { + Assert(value(c[i]) == l_Undef); + uncheckedEnqueue(~c[i]); + } + } - bool result = propagate(CHECK_WITHOUT_THEORY) != CRef_Undef; - cancelUntil(0); - return result; + bool result = propagate(CHECK_WITHOUT_THEORY) != CRef_Undef; + cancelUntil(0); + return result; } @@ -380,7 +385,7 @@ bool SimpSolver::backwardSubsumptionCheck(bool verbose) int cnt = 0; int subsumed = 0; int deleted_literals = 0; - assert(decisionLevel() == 0); + Assert(decisionLevel() == 0); while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){ @@ -405,7 +410,9 @@ bool SimpSolver::backwardSubsumptionCheck(bool verbose) if (verbose && verbosity >= 2 && cnt++ % 1000 == 0) printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals); - assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated before this point. + Assert(c.size() > 1 + || value(c[0]) == l_True); // Unit-clauses should have been + // propagated before this point. // Find best variable to scan: Var best = var(c[0]); @@ -445,7 +452,7 @@ bool SimpSolver::backwardSubsumptionCheck(bool verbose) bool SimpSolver::asymm(Var v, CRef cr) { Clause& c = ca[cr]; - assert(decisionLevel() == 0); + Assert(decisionLevel() == 0); if (c.mark() || satisfied(c)) return true; @@ -471,18 +478,16 @@ bool SimpSolver::asymm(Var v, CRef cr) bool SimpSolver::asymmVar(Var v) { - assert(use_simplification); + Assert(use_simplification); - const vec<CRef>& cls = occurs.lookup(v); + const vec<CRef>& cls = occurs.lookup(v); - if (value(v) != l_Undef || cls.size() == 0) - return true; + if (value(v) != l_Undef || cls.size() == 0) return true; - for (int i = 0; i < cls.size(); i++) - if (!asymm(v, cls[i])) - return false; + for (int i = 0; i < cls.size(); i++) + if (!asymm(v, cls[i])) return false; - return backwardSubsumptionCheck(); + return backwardSubsumptionCheck(); } @@ -505,7 +510,7 @@ static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c) if (var(c[i]) == v) v_pos = i + first; } - assert(v_pos != -1); + Assert(v_pos != -1); // Swap the first literal with the 'v' literal, so that the literal // containing 'v' will occur first in the clause: @@ -521,44 +526,48 @@ static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c) bool SimpSolver::eliminateVar(Var v) { - assert(!frozen[v]); - assert(!isEliminated(v)); - assert(value(v) == l_Undef); - - // Split the occurrences into positive and negative: - // - const vec<CRef>& cls = occurs.lookup(v); - vec<CRef> pos, neg; - for (int i = 0; i < cls.size(); i++) - (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]); - - // Check whether the increase in number of clauses stays within the allowed ('grow'). Moreover, no - // clause must exceed the limit on the maximal clause size (if it is set): - // - int cnt = 0; - int clause_size = 0; + Assert(!frozen[v]); + Assert(!isEliminated(v)); + Assert(value(v) == l_Undef); + + // Split the occurrences into positive and negative: + // + const vec<CRef>& cls = occurs.lookup(v); + vec<CRef> pos, neg; + for (int i = 0; i < cls.size(); i++) + (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]); + + // Check whether the increase in number of clauses stays within the allowed + // ('grow'). Moreover, no clause must exceed the limit on the maximal clause + // size (if it is set): + // + int cnt = 0; + int clause_size = 0; + + for (int i = 0; i < pos.size(); i++) + for (int j = 0; j < neg.size(); j++) + if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) + && (++cnt > cls.size() + grow + || (clause_lim != -1 && clause_size > clause_lim))) + return true; + // Delete and store old clauses: + eliminated[v] = true; + setDecisionVar(v, false); + eliminated_vars++; + + if (pos.size() > neg.size()) + { + for (int i = 0; i < neg.size(); i++) + mkElimClause(elimclauses, v, ca[neg[i]]); + mkElimClause(elimclauses, mkLit(v)); + } + else + { for (int i = 0; i < pos.size(); i++) - for (int j = 0; j < neg.size(); j++) - if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) - && (++cnt > cls.size() + grow - || (clause_lim != -1 && clause_size > clause_lim))) - return true; - - // Delete and store old clauses: - eliminated[v] = true; - setDecisionVar(v, false); - eliminated_vars++; - - if (pos.size() > neg.size()){ - for (int i = 0; i < neg.size(); i++) - mkElimClause(elimclauses, v, ca[neg[i]]); - mkElimClause(elimclauses, mkLit(v)); - }else{ - for (int i = 0; i < pos.size(); i++) - mkElimClause(elimclauses, v, ca[pos[i]]); - mkElimClause(elimclauses, ~mkLit(v)); - } + mkElimClause(elimclauses, v, ca[pos[i]]); + mkElimClause(elimclauses, ~mkLit(v)); + } for (int i = 0; i < cls.size(); i++) removeClause(cls[i]); @@ -587,32 +596,35 @@ bool SimpSolver::eliminateVar(Var v) bool SimpSolver::substitute(Var v, Lit x) { - assert(!frozen[v]); - assert(!isEliminated(v)); - assert(value(v) == l_Undef); + Assert(!frozen[v]); + Assert(!isEliminated(v)); + Assert(value(v) == l_Undef); - if (!ok) return false; + if (!ok) return false; - eliminated[v] = true; - setDecisionVar(v, false); - const vec<CRef>& cls = occurs.lookup(v); + eliminated[v] = true; + setDecisionVar(v, false); + const vec<CRef>& cls = occurs.lookup(v); - vec<Lit>& subst_clause = add_tmp; - for (int i = 0; i < cls.size(); i++){ - Clause& c = ca[cls[i]]; + vec<Lit>& subst_clause = add_tmp; + for (int i = 0; i < cls.size(); i++) + { + Clause& c = ca[cls[i]]; - subst_clause.clear(); - for (int j = 0; j < c.size(); j++){ - Lit p = c[j]; - subst_clause.push(var(p) == v ? x ^ sign(p) : p); - } + subst_clause.clear(); + for (int j = 0; j < c.size(); j++) + { + Lit p = c[j]; + subst_clause.push(var(p) == v ? x ^ sign(p) : p); + } - removeClause(cls[i]); - ClauseId id = ClauseIdUndef; - if (!addClause_(subst_clause, c.removable(), id)) { - return ok = false; - } + removeClause(cls[i]); + ClauseId id = ClauseIdUndef; + if (!addClause_(subst_clause, c.removable(), id)) + { + return ok = false; } + } return true; } @@ -657,11 +669,12 @@ bool SimpSolver::eliminate(bool turn_off_elim) // Empty elim_heap and return immediately on user-interrupt: if (asynch_interrupt){ - assert(bwdsub_assigns == trail.size()); - assert(subsumption_queue.size() == 0); - assert(n_touched == 0); - elim_heap.clear(); - goto cleanup; } + Assert(bwdsub_assigns == trail.size()); + Assert(subsumption_queue.size() == 0); + Assert(n_touched == 0); + elim_heap.clear(); + goto cleanup; + } // printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size()); for (int cnt = 0; !elim_heap.empty(); cnt++){ @@ -690,7 +703,7 @@ bool SimpSolver::eliminate(bool turn_off_elim) checkGarbage(simp_garbage_frac); } - assert(subsumption_queue.size() == 0); + Assert(subsumption_queue.size() == 0); } cleanup: diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index f952aee1e..5e348c1e7 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -21,12 +21,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_SimpSolver_h #define Minisat_SimpSolver_h +#include "base/check.h" #include "cvc4_private.h" - #include "proof/clause_id.h" -#include "prop/minisat/mtl/Queue.h" #include "prop/minisat/core/Solver.h" - +#include "prop/minisat/mtl/Queue.h" namespace CVC4 { namespace prop { @@ -204,11 +203,12 @@ class SimpSolver : public Solver { inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v]; } inline void SimpSolver::updateElimHeap(Var v) { - assert(use_simplification); - // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef) - if (elim_heap.inHeap(v) || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)) - elim_heap.update(v); } - + Assert(use_simplification); + // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef) + if (elim_heap.inHeap(v) + || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)) + elim_heap.update(v); +} inline bool SimpSolver::addClause(const vec<Lit>& ps, bool removable, ClauseId& id) { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, id); } diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp index ebfda01a8..4d948415f 100644 --- a/src/util/rational_cln_imp.cpp +++ b/src/util/rational_cln_imp.cpp @@ -51,6 +51,23 @@ Rational Rational::fromDecimal(const std::string& dec) { } } +int Rational::sgn() const +{ + if (cln::zerop(d_value)) + { + return 0; + } + else if (cln::minusp(d_value)) + { + return -1; + } + else + { + Assert(cln::plusp(d_value)); + return 1; + } +} + std::ostream& operator<<(std::ostream& os, const Rational& q){ return os << q.toString(); } diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index d7ff55344..6d83a5a0f 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -29,7 +29,6 @@ #include <cln/rational_io.h> #include <cln/real.h> -#include <cassert> #include <sstream> #include <string> @@ -210,22 +209,7 @@ class CVC4_PUBLIC Rational return cln::compare(d_value, x.d_value); } - int sgn() const - { - if (cln::zerop(d_value)) - { - return 0; - } - else if (cln::minusp(d_value)) - { - return -1; - } - else - { - assert(cln::plusp(d_value)); - return 1; - } - } + int sgn() const; bool isZero() const { return cln::zerop(d_value); } |