| /******************************************************************************* |
| * Copyright (c) 2016 CEA LIST. |
| * |
| * All rights reserved. This program and the accompanying materials |
| * are made available under the terms of the Eclipse Public License v1.0 |
| * which accompanies this distribution, and is available at |
| * http://www.eclipse.org/legal/epl-v10.html |
| * |
| * Created on: 29 févr. 2012 |
| * |
| * Contributors: |
| * Arnault Lapitre (CEA LIST) arnault.lapitre@cea.fr |
| * - Initial API and implementation |
| ******************************************************************************/ |
| |
| #include "Z3Solver.h" |
| |
| /* |
| * Here because "SolverDef.h" could define this macro |
| */ |
| #if defined( _AVM_SOLVER_Z3_ ) |
| |
| |
| #include <util/avm_vfs.h> |
| |
| #include <fml/expression/AvmCode.h> |
| #include <fml/builtin/Boolean.h> |
| #include <fml/builtin/Character.h> |
| #include <fml/expression/BuiltinContainer.h> |
| #include <fml/expression/ExpressionComparer.h> |
| #include <fml/expression/ExpressionConstructor.h> |
| #include <fml/expression/ExpressionFactory.h> |
| #include <fml/expression/ExpressionTypeChecker.h> |
| #include <fml/numeric/Float.h> |
| #include <fml/numeric/Integer.h> |
| #include <fml/numeric/Rational.h> |
| |
| #include <fml/operator/Operator.h> |
| |
| #include <fml/runtime/ExecutionContext.h> |
| #include <fml/runtime/ExecutionData.h> |
| #include <fml/runtime/RuntimeForm.h> |
| #include <fml/runtime/RuntimeID.h> |
| #include <fml/runtime/TableOfData.h> |
| |
| #include <fml/type/TypeManager.h> |
| |
| #include <fml/workflow/WObject.h> |
| |
| #include <fstream> |
| |
| |
| namespace sep |
| { |
| |
| /* |
| ******************************************************************************* |
| * ID |
| ******************************************************************************* |
| */ |
| std::string Z3Solver::ID = "Z3"; |
| |
| std::string Z3Solver::DESCRIPTION = "Z3 " |
| "'High-performance Theorem Prover at Microsoft Research, MIT License'"; |
| |
| avm_uint64_t Z3Solver::SOLVER_SESSION_ID = 0; |
| |
| |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| |
| |
| #if defined( _AVM_SOLVER_Z3_CPP_ ) |
| |
| |
| /** |
| * CREATE - DESTROY |
| * ValidityChecker |
| */ |
| |
| |
| bool Z3Solver::createChecker(z3::config & cfg, z3::context & ctx) |
| { |
| CFG = & cfg; |
| |
| CFG->set("MODEL", "true"); |
| |
| CTX = & ctx; |
| |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| ++SOLVER_SESSION_ID; |
| AVM_IF_DEBUG_LEVEL_GTE_HIGH |
| mLogFolderLocation = OSS << VFS::ProjectLogPath << "/z3/"; |
| |
| if ( not VFS::checkWritingFolder(mLogFolderLocation) ) |
| { |
| AVM_OS_LOG << " Z3Solver::createChecker :> Error: The folder " |
| << "`" << mLogFolderLocation << "' " |
| << "---> doesn't exist or is not writable !!!" |
| << std::endl << std::endl; |
| return( false ); |
| } |
| AVM_ENDIF_DEBUG_LEVEL_GTE_HIGH |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| |
| SMT_CST_BOOL_TRUE = CTX->bool_val(true); |
| SMT_CST_BOOL_FALSE = CTX->bool_val(false); |
| |
| resetTable(); |
| |
| return( true ); |
| } |
| |
| |
| bool Z3Solver::destroyChecker() |
| { |
| resetTable(); |
| |
| CFG = NULL; |
| |
| CTX = NULL; |
| |
| return( true ); |
| } |
| |
| bool Z3Solver::resetTable() |
| { |
| base_this_type::resetTable(); |
| |
| mTableOfParameterDecl.append( z3::symbol(*CTX, 0) ); |
| |
| mTableOfParameterExpr.append( z3::expr(*CTX) ); |
| |
| return( true ); |
| } |
| |
| |
| |
| /** |
| * PROVER |
| */ |
| bool Z3Solver::isSubSet( |
| const ExecutionContext & newEC, const ExecutionContext & oldEC) |
| { |
| return( true ); |
| } |
| |
| bool Z3Solver::isEqualSet( |
| const ExecutionContext & newEC, const ExecutionContext & oldEC) |
| { |
| return( true ); |
| } |
| |
| SolverDef::SATISFIABILITY_RING Z3Solver::isSatisfiable(const BF & aCondition) |
| { |
| SolverDef::SATISFIABILITY_RING satisfiability = SolverDef::SATISFIABLE; |
| |
| z3::config cfg; |
| z3::context ctx; |
| createChecker(cfg, ctx); |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| AVM_OS_TRACE << "Z3Solver::isSatisfiable(...) " |
| ":" << SOLVER_SESSION_ID << ">" << std::endl |
| << "\t" << aCondition.str() << std::endl; |
| |
| // trace to file |
| AVM_IF_DEBUG_LEVEL_GTE_HIGH |
| smt_check_sat(aCondition); |
| AVM_ENDIF_DEBUG_LEVEL_GTE_HIGH |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| |
| z3::expr z3Condition = from_baseform(aCondition); |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| AVM_OS_TRACE << "Z3Condition :" << SOLVER_SESSION_ID << ">" << std::endl |
| << "\t" << z3Condition << std::endl; |
| AVM_IF_DEBUG_LEVEL_GTE_HIGH |
| AVM_OS_TRACE << "Z3::CTX :" << SOLVER_SESSION_ID << ">" << std::endl |
| << ctx << std::endl; |
| AVM_ENDIF_DEBUG_LEVEL_GTE_HIGH |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| |
| //if( z3Condition != NULL ) |
| { |
| z3::solver z3Solver(*CTX); |
| |
| z3Solver.add( z3Condition ); |
| |
| switch( z3Solver.check() ) |
| { |
| case z3::sat: |
| { |
| satisfiability = SolverDef::SATISFIABLE; |
| break; |
| } |
| |
| case z3::unsat: |
| { |
| satisfiability = SolverDef::UNSATISFIABLE; |
| break; |
| } |
| |
| case z3::unknown: |
| { |
| satisfiability = SolverDef::UNKNOWN_SAT; |
| break; |
| } |
| |
| default: |
| { |
| satisfiability = SolverDef::ABORT_SAT; |
| break; |
| } |
| } |
| } |
| |
| destroyChecker(); |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| AVM_OS_TRACE << "result :" << SOLVER_SESSION_ID << "> " |
| << SolverDef::strSatisfiability(satisfiability) << std::endl; |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| |
| return( satisfiability ); |
| } |
| |
| |
| /** |
| * SOLVER |
| */ |
| bool Z3Solver::solveImpl(const BF & aCondition, |
| BFVector & dataVector, BFVector & valuesVector) |
| { |
| SolverDef::SATISFIABILITY_RING satisfiability = SolverDef::SATISFIABLE; |
| |
| z3::config cfg; |
| z3::context ctx; |
| createChecker(cfg, ctx); |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| AVM_OS_TRACE << "Z3Solver::solve(...) :" |
| << SOLVER_SESSION_ID << ">" << std::endl |
| << "\t" << aCondition.str() << std::endl; |
| |
| // trace to file |
| smt_check_model(aCondition, dataVector, valuesVector); |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| |
| z3::expr z3Condition = from_baseform(aCondition); |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| AVM_OS_TRACE << "Z3Condition :" << SOLVER_SESSION_ID << ">" << std::endl |
| << "\t" << z3Condition << std::endl; |
| AVM_IF_DEBUG_LEVEL_GTE_HIGH |
| AVM_OS_TRACE << "Z3::CTX :" << SOLVER_SESSION_ID << ">" << std::endl |
| << ctx << std::endl; |
| AVM_ENDIF_DEBUG_LEVEL_GTE_HIGH |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| |
| z3::solver z3Solver(*CTX); |
| |
| z3Solver.add( z3Condition ); |
| |
| switch( z3Solver.check() ) |
| { |
| case z3::sat: |
| { |
| satisfiability = SolverDef::SATISFIABLE; |
| break; |
| } |
| |
| case z3::unsat: |
| { |
| satisfiability = SolverDef::UNSATISFIABLE; |
| break; |
| } |
| |
| case z3::unknown: |
| { |
| satisfiability = SolverDef::UNKNOWN_SAT; |
| break; |
| } |
| |
| default: |
| { |
| satisfiability = SolverDef::ABORT_SAT; |
| break; |
| } |
| } |
| |
| //if( z3Condition != NULL ) |
| { |
| z3::solver z3Solver(*CTX); |
| |
| z3Solver.add( z3Condition ); |
| |
| switch( z3Solver.check() ) |
| { |
| case z3::sat: |
| { |
| satisfiability = SolverDef::SATISFIABLE; |
| |
| z3::model z3Model = z3Solver.get_model(); |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| AVM_OS_TRACE << "Z3Model sat:" << SOLVER_SESSION_ID << ">" |
| << std::endl << z3Model << std::endl; |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| |
| unsigned num_constants = z3Model.num_consts(); |
| for( unsigned i = 0 ; i < num_constants ; i++ ) |
| { |
| z3::func_decl paramDecl = z3Model.get_const_decl(i); |
| |
| z3::symbol paramSymbol = z3Model.get_const_decl(i).name(); |
| |
| z3::expr value = z3Model.get_const_interp(paramDecl); |
| |
| int offset = mTableOfParameterDecl.find(paramSymbol); |
| if( offset >= 0 ) |
| { |
| dataVector.append( mTableOfParameterInstance[offset] ); |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| AVM_OS_TRACE << paramSymbol << " := "; |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| |
| BF bfVal = to_baseform( z3Model, value); |
| |
| valuesVector.append( bfVal.valid() ? |
| bfVal : dataVector.back() ); |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| AVM_OS_TRACE << value << std::endl; |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| } |
| else |
| { |
| AVM_OS_FATAL_ERROR_EXIT |
| << "Z3Solver::solve :> unfound " |
| "parameter instance for Z3 symbol << " |
| << paramSymbol << " >> !!!" |
| << SEND_EXIT; |
| } |
| } |
| |
| |
| break; |
| break; |
| } |
| |
| case z3::unsat: |
| { |
| satisfiability = SolverDef::UNSATISFIABLE; |
| break; |
| } |
| |
| case z3::unknown: |
| { |
| satisfiability = SolverDef::UNKNOWN_SAT; |
| |
| break; |
| } |
| |
| default: |
| { |
| satisfiability = SolverDef::ABORT_SAT; |
| break; |
| } |
| } |
| } |
| |
| destroyChecker(); |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| AVM_OS_TRACE << "solve :" << SOLVER_SESSION_ID << "> " |
| << SolverDef::strSatisfiability(satisfiability) << std::endl; |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| |
| return( satisfiability == SolverDef::SATISFIABLE ); |
| } |
| |
| |
| |
| /** |
| * TOOLS |
| */ |
| z3::sort Z3Solver::getZ3Type(BaseTypeSpecifier * bts) |
| { |
| if( bts->isTypedBoolean() ) |
| { |
| return( CTX->bool_sort() ); |
| } |
| |
| else if( bts->isTypedEnum() ) |
| { |
| return( CTX->int_sort() ); |
| // TODO Attention : il faudrait rajouter les contraintes |
| // d'intervalle pour le type énuméré |
| } |
| else if( bts->weaklyTypedInteger() ) |
| { |
| return( CTX->int_sort() ); |
| } |
| |
| else if( bts->weaklyTypedReal() ) |
| { |
| return( CTX->real_sort() ); |
| } |
| |
| return( CTX->real_sort() ); |
| } |
| |
| |
| z3::expr Z3Solver::getParameterExpr(const BF & bfParameter) |
| { |
| InstanceOfData * aParameter = bfParameter.to_ptr< InstanceOfData >(); |
| |
| if( aParameter->getMark() == 0 ) |
| { |
| aParameter->setMark( mTableOfParameterInstance.size() ); |
| mTableOfParameterInstance.append( bfParameter ); |
| |
| mTableOfParameterDecl.push_back( |
| CTX->str_symbol(aParameter->getNameID().c_str()) ); |
| |
| mTableOfParameterExpr.push_back( |
| CTX->constant(mTableOfParameterDecl.last(), |
| getZ3Type(aParameter->referedTypeSpecifier())) ); |
| } |
| |
| return( mTableOfParameterExpr.at( aParameter->getMark() ) ); |
| } |
| |
| |
| |
| |
| z3::expr Z3Solver::getVariableExpr(InstanceOfData * aVar, std::size_t varID) |
| { |
| if( mTableOfVariableExpr.size() <= varID ) |
| { |
| mTableOfVariableDecl.push_back( |
| CTX->str_symbol(aVar->getNameID().c_str()) ); |
| |
| mTableOfVariableExpr.push_back( |
| CTX->constant(mTableOfVariableDecl.last(), |
| getZ3Type(aVar->getTypeSpecifier())) ); |
| } |
| |
| return( mTableOfVariableExpr.at( varID ) ); |
| } |
| |
| |
| z3::expr Z3Solver::safe_from_baseform(const BF & exprForm, |
| BaseTypeSpecifier * typeSpecifier) |
| { |
| z3::expr e(*CTX); |
| |
| try |
| { |
| e = from_baseform(exprForm, typeSpecifier); |
| |
| destroyChecker(); |
| } |
| catch ( ... ) |
| { |
| AVM_OS_WARN << std::endl << REPEAT("********", 10) << std::endl |
| << "\tZ3Solver::safe_from_baseform< unknown::exception :" |
| << SOLVER_SESSION_ID << ">" << std::endl |
| << REPEAT("--------", 10) << std::endl |
| << "\tFailed to CONVERT sep::fml::expression to Z3::Expr:>" << std::endl |
| << "\t " << exprForm.str(" ") << std::endl |
| << REPEAT("********", 10) << std::endl; |
| |
| destroyChecker(); |
| } |
| |
| return( e ); |
| } |
| |
| |
| z3::expr Z3Solver::from_baseform(const BF & exprForm, |
| BaseTypeSpecifier * typeSpecifier) |
| { |
| AVM_OS_ASSERT_FATAL_NULL_SMART_POINTER_EXIT( exprForm ) << "expression !!!" |
| << SEND_EXIT; |
| |
| |
| switch( exprForm.classKind() ) |
| { |
| case FORM_AVMCODE_KIND: |
| { |
| AvmCode * aCode = exprForm.to_ptr< AvmCode >(); |
| |
| typeSpecifier = TypeManager::UNIVERSAL; |
| |
| switch( aCode->getAvmOpCode() ) |
| { |
| // COMPARISON OPERATION |
| case AVM_OPCODE_EQ: |
| { |
| return( from_baseform(aCode->first() , typeSpecifier) == |
| from_baseform(aCode->second(), typeSpecifier) ); |
| } |
| |
| case AVM_OPCODE_NEQ: |
| { |
| return( from_baseform(aCode->first() , typeSpecifier) != |
| from_baseform(aCode->second(), typeSpecifier) ); |
| |
| // ARGS arg( 2 ); |
| // |
| // arg.next( from_baseform(aCode->first() , typeSpecifier) ); |
| // arg.next( from_baseform(aCode->second(), typeSpecifier) ); |
| // |
| // return( Z3_mk_distinct(CTX, 2, arg->table) ); |
| } |
| |
| case AVM_OPCODE_LT: |
| { |
| return( from_baseform(aCode->first() , typeSpecifier) < |
| from_baseform(aCode->second(), typeSpecifier) ); |
| } |
| |
| case AVM_OPCODE_LTE: |
| { |
| return( from_baseform(aCode->first() , typeSpecifier) <= |
| from_baseform(aCode->second(), typeSpecifier) ); |
| } |
| |
| case AVM_OPCODE_GT: |
| { |
| return( from_baseform(aCode->first() , typeSpecifier) > |
| from_baseform(aCode->second(), typeSpecifier) ); |
| } |
| |
| case AVM_OPCODE_GTE: |
| { |
| return( from_baseform(aCode->first() , typeSpecifier) >= |
| from_baseform(aCode->second(), typeSpecifier) ); |
| } |
| |
| |
| case AVM_OPCODE_CONTAINS: |
| { |
| BuiltinCollection * aCollection = |
| aCode->first().to_ptr< BuiltinCollection >(); |
| |
| if( aCollection->singleton() ) |
| { |
| return( from_baseform(aCollection->at(0), typeSpecifier) == |
| from_baseform(aCode->second(), typeSpecifier) ); |
| } |
| else if( aCollection->populated() ) |
| { |
| std::size_t colSize = aCollection->size(); |
| const BF & elt = aCode->second(); |
| |
| z3::expr z3Or = ( from_baseform(elt, typeSpecifier) == |
| from_baseform(aCollection->at(0), typeSpecifier) ); |
| |
| for( std::size_t offset = 1 ; offset < colSize ; ++offset ) |
| { |
| z3Or = z3Or || (from_baseform(elt, typeSpecifier) == |
| from_baseform(aCollection->at(offset), typeSpecifier)); |
| } |
| |
| return( z3Or ); |
| } |
| else |
| { |
| return( ((typeSpecifier != NULL) && |
| typeSpecifier->isTypedBoolean()) ? |
| CTX->bool_val(false) : CTX->int_val(0) ); |
| } |
| } |
| |
| |
| // LOGICAL OPERATION |
| case AVM_OPCODE_NOT: |
| { |
| return( not from_baseform( |
| aCode->first(), TypeManager::BOOLEAN) ); |
| } |
| |
| case AVM_OPCODE_AND: |
| { |
| z3::expr z3And = |
| from_baseform(aCode->first(), TypeManager::BOOLEAN) && |
| from_baseform(aCode->second(), TypeManager::BOOLEAN); |
| |
| for( std::size_t offset = 2 ; offset < aCode->size() ; ++offset ) |
| { |
| z3And = z3And && from_baseform( |
| aCode->at(offset), TypeManager::BOOLEAN); |
| } |
| |
| return( z3And ); |
| } |
| |
| case AVM_OPCODE_NAND: |
| { |
| z3::expr z3And = |
| from_baseform(aCode->first(), TypeManager::BOOLEAN) && |
| from_baseform(aCode->second(), TypeManager::BOOLEAN); |
| |
| for( std::size_t offset = 2 ; offset < aCode->size() ; ++offset ) |
| { |
| z3And = z3And && from_baseform( |
| aCode->at(offset), TypeManager::BOOLEAN); |
| } |
| |
| return( not z3And ); |
| } |
| |
| // case AVM_OPCODE_XAND: |
| |
| case AVM_OPCODE_OR: |
| { |
| z3::expr z3Or = |
| from_baseform(aCode->first(), TypeManager::BOOLEAN) || |
| from_baseform(aCode->second(), TypeManager::BOOLEAN); |
| |
| for( std::size_t offset = 2 ; offset < aCode->size() ; ++offset ) |
| { |
| z3Or = z3Or || from_baseform( |
| aCode->at(offset), TypeManager::BOOLEAN); |
| } |
| |
| return( z3Or ); |
| } |
| |
| case AVM_OPCODE_NOR: |
| { |
| z3::expr z3Or = |
| from_baseform(aCode->first(), TypeManager::BOOLEAN) || |
| from_baseform(aCode->second(), TypeManager::BOOLEAN); |
| |
| for( std::size_t offset = 2 ; offset < aCode->size() ; ++offset ) |
| { |
| z3Or = z3Or || from_baseform( |
| aCode->at(offset), TypeManager::BOOLEAN); |
| } |
| |
| return( not z3Or ); |
| } |
| |
| |
| // BITWISE OPERATION |
| // case AVM_OPCODE_BAND: |
| // case AVM_OPCODE_BOR: |
| // case AVM_OPCODE_LSHIFT: |
| // case AVM_OPCODE_RSHIFT: |
| |
| case AVM_OPCODE_XOR: |
| { |
| z3::expr arg0 = from_baseform( |
| aCode->first(), TypeManager::BOOLEAN); |
| |
| z3::expr arg1 = from_baseform( |
| aCode->second(), TypeManager::BOOLEAN); |
| |
| return( (arg0 && (! arg1)) || ((! arg0) && arg1) ); |
| } |
| |
| // case AVM_OPCODE_XNOR: |
| |
| |
| // ARITHMETIC OPERATION |
| case AVM_OPCODE_PLUS: |
| { |
| z3::expr z3Plus = |
| from_baseform(aCode->first(), typeSpecifier) + |
| from_baseform(aCode->second(), typeSpecifier); |
| |
| for( std::size_t offset = 2 ; offset < aCode->size() ; ++offset ) |
| { |
| z3Plus = z3Plus + |
| from_baseform(aCode->at(offset), typeSpecifier); |
| } |
| |
| return( z3Plus ); |
| } |
| |
| case AVM_OPCODE_UMINUS: |
| { |
| return( - from_baseform(aCode->first(), typeSpecifier) ); |
| } |
| |
| case AVM_OPCODE_MINUS: |
| { |
| z3::expr z3Minus = |
| from_baseform(aCode->first(), typeSpecifier) - |
| from_baseform(aCode->second(), typeSpecifier); |
| |
| for( std::size_t offset = 2 ; offset < aCode->size() ; ++offset ) |
| { |
| z3Minus = z3Minus - |
| from_baseform(aCode->at(offset), typeSpecifier); |
| } |
| |
| return( z3Minus ); |
| } |
| |
| case AVM_OPCODE_MULT: |
| { |
| z3::expr z3Mult = |
| from_baseform(aCode->first(), typeSpecifier) * |
| from_baseform(aCode->second(), typeSpecifier); |
| |
| for( std::size_t offset = 2 ; offset < aCode->size() ; ++offset ) |
| { |
| z3Mult = z3Mult * |
| from_baseform(aCode->at(offset), typeSpecifier); |
| } |
| |
| return( z3Mult ); |
| } |
| |
| case AVM_OPCODE_DIV: |
| { |
| return( from_baseform(aCode->first() , typeSpecifier) / |
| from_baseform(aCode->second(), typeSpecifier) ); |
| } |
| |
| case AVM_OPCODE_POW: |
| { |
| |
| // if( ExpressionFactory::isInt32(aCode->second()) ) |
| // { |
| // return( std::pw( |
| // from_baseform(aCode->first() , typeSpecifier), |
| // from_baseform(aCode->second() , typeSpecifier) ) ); |
| // } |
| // else |
| { |
| AVM_OS_FATAL_ERROR_EXIT |
| << "Z3Solver::from_baseform:> " |
| "Unsupported expression Operator " |
| "<< AVM_OPCODE_POW >> !!!" |
| << SEND_EXIT; |
| |
| return( z3::expr(*CTX) ); |
| } |
| } |
| |
| // case AVM_OPCODE_MOD: |
| |
| default: |
| { |
| AVM_OS_FATAL_ERROR_EXIT |
| << "Z3Solver::from_baseform:> " |
| "Unexpected expression !!!\n" |
| << aCode->toString( AVM_TAB1_INDENT ) |
| << SEND_EXIT; |
| |
| return( z3::expr(*CTX) ); |
| } |
| } |
| |
| break; |
| } |
| |
| case FORM_INSTANCE_DATA_KIND: |
| { |
| return( getParameterExpr( exprForm ) ); |
| } |
| |
| case FORM_BUILTIN_BOOLEAN_KIND: |
| { |
| return( CTX->bool_val( |
| exprForm.to_ptr< Boolean >()->getValue() ) ); |
| } |
| |
| case FORM_BUILTIN_INTEGER_KIND: |
| { |
| if( (typeSpecifier != NULL) && typeSpecifier->isTypedBoolean() ) |
| { |
| // return( CTX->bool_val( |
| // not exprForm.to_ptr< Integer >()->isZero() ) ); |
| |
| return( exprForm.to_ptr< Integer >()->isZero() ? |
| SMT_CST_BOOL_FALSE : SMT_CST_BOOL_TRUE ); |
| } |
| else |
| { |
| #if defined( _AVM_BUILTIN_NUMERIC_GMP_ ) |
| |
| return( CTX->int_val( static_cast< __int64 >( |
| exprForm.to_ptr< Integer >()->toInteger() ) ) ); |
| |
| #else |
| |
| return( CTX->int_val( static_cast< __int64 >( |
| exprForm.to_ptr< Integer >()->toInteger() ) ) ); |
| |
| #endif /* _AVM_BUILTIN_NUMERIC_GMP_ */ |
| } |
| |
| // return( CTX->int_val( exprForm.to_ptr< Integer >()->str().c_str() ) ); |
| } |
| |
| case FORM_BUILTIN_RATIONAL_KIND: |
| { |
| if( (typeSpecifier != NULL) && typeSpecifier->isTypedBoolean() ) |
| { |
| // return( CTX->bool_val( |
| // not exprForm.to_ptr< Rational >()->isZero() ) ); |
| |
| return( exprForm.to_ptr< Rational >()->isZero() ? |
| SMT_CST_BOOL_FALSE : SMT_CST_BOOL_TRUE ); |
| } |
| else |
| { |
| #if defined( _AVM_BUILTIN_NUMERIC_GMP_ ) |
| |
| return( CTX->real_val( |
| exprForm.to_ptr< Rational >()->toNumerator(), |
| exprForm.to_ptr< Rational >()->toDenominator() ) ); |
| |
| #else |
| |
| return( CTX->real_val( |
| exprForm.to_ptr< Rational >()->toNumerator(), |
| exprForm.to_ptr< Rational >()->toDenominator() ) ); |
| |
| #endif /* _AVM_BUILTIN_NUMERIC_GMP_ */ |
| } |
| |
| // return( CTX->real_val( exprForm.to_ptr< Rational >()->str().c_str() ) ); |
| } |
| |
| case FORM_BUILTIN_FLOAT_KIND: |
| { |
| if( (typeSpecifier != NULL) && typeSpecifier->isTypedBoolean() ) |
| { |
| // return( CTX->bool_val( |
| // not exprForm.to_ptr< Float >()->isZero() ) ); |
| |
| return( exprForm.to_ptr< Float >()->isZero() ? |
| SMT_CST_BOOL_FALSE : SMT_CST_BOOL_TRUE ); |
| } |
| else |
| { |
| #if defined( _AVM_BUILTIN_NUMERIC_GMP_ ) |
| |
| return( CTX->real_val( |
| exprForm.to_ptr< Float >()->str().c_str() ) ); |
| |
| #else |
| |
| return( CTX->real_val( |
| exprForm.to_ptr< Float >()->str().c_str() ) ); |
| |
| #endif /* _AVM_BUILTIN_NUMERIC_GMP_ */ |
| } |
| } |
| |
| |
| case FORM_RUNTIME_ID_KIND: |
| { |
| return( CTX->int_val( exprForm.bfRID().getRid() ) ); |
| } |
| |
| default: |
| { |
| AVM_OS_FATAL_ERROR_EXIT |
| << "Z3Solver::from_baseform:> Unexpected BASEFORM KIND << " |
| << exprForm.classKindName() << " >> as expression << " |
| << exprForm.str() << " >> !!!" |
| << SEND_EXIT; |
| |
| return( z3::expr(*CTX) ); |
| } |
| } |
| |
| AVM_OS_FATAL_ERROR_EXIT |
| << "Z3Solver::from_baseform ERROR !!!" |
| << SEND_EXIT; |
| |
| return( z3::expr(*CTX) ); |
| } |
| |
| |
| BF Z3Solver::to_baseform(z3::model z3Model, z3::expr z3Form) |
| { |
| std::ostringstream oss; |
| oss << z3Form; |
| |
| if( z3Form.is_bool() ) |
| { |
| return( ExpressionConstructor::newBoolean( oss.str() ) ); |
| } |
| else if( z3Form.is_int() ) |
| { |
| return( ExpressionConstructor::newInteger( oss.str() ) ); |
| } |
| else if( z3Form.is_real() ) |
| { |
| return( ExpressionConstructor::newFloat( oss.str() ) ); |
| } |
| |
| return( BF::REF_NULL ); |
| } |
| |
| |
| /** |
| * Using file API |
| */ |
| |
| SolverDef::SATISFIABILITY_RING Z3Solver::smt_check_sat(const BF & aCondition) |
| { |
| SolverDef::SATISFIABILITY_RING satisfiability = SolverDef::SATISFIABLE; |
| |
| BFVector paramVector; |
| |
| StringOutStream ossCondition("", "\t", ""); |
| to_smt(ossCondition, aCondition, paramVector); |
| |
| std::string fileLocation = OSS << mLogFolderLocation, |
| << "z3_check_sat_" << SOLVER_SESSION_ID << ".smt"; |
| std::ofstream osFile; |
| osFile.open(fileLocation.c_str(), std::ios_base::out); |
| if ( osFile.good() ) |
| { |
| // osFile << "(echo \"" << aCondition.str() << "\")" << std::endl; |
| |
| InstanceOfData * aParam; |
| |
| std::size_t paramCount = paramVector.size(); |
| for( std::size_t offset = 0 ; offset < paramCount ; offset++ ) |
| { |
| aParam = paramVector[ offset ].to_ptr< InstanceOfData >(); |
| |
| osFile << "(declare-const " << aParam->getFullyQualifiedNameID() |
| << " "; |
| if( aParam->isTypedBoolean() ) |
| { |
| osFile << "Bool"; |
| } |
| else if( aParam->weaklyTypedInteger() || |
| aParam->isTypedEnum() ) |
| { |
| osFile << "Int"; |
| } |
| else if( aParam->weaklyTypedReal() ) |
| { |
| osFile << "Real"; |
| } |
| else |
| { |
| osFile << "Unknown"; |
| } |
| osFile << ")" << std::endl; |
| } |
| |
| osFile << "(assert " << ossCondition.str() << ")" << std::endl; |
| |
| osFile << "(check-sat)" << std::endl; |
| |
| osFile.close(); |
| } |
| else |
| { |
| return( SolverDef::ABORT_SAT ); |
| } |
| |
| |
| return( satisfiability ); |
| } |
| |
| bool Z3Solver::smt_check_model(const BF & aCondition, |
| BFVector & dataVector, BFVector & valuesVector) |
| { |
| BFVector paramVector; |
| |
| StringOutStream ossCondition("", "\t", ""); |
| to_smt(ossCondition, aCondition, paramVector); |
| |
| std::string fileLocation = OSS << mLogFolderLocation |
| << "z3_check_sat_" << SOLVER_SESSION_ID << ".smt"; |
| std::ofstream osFile; |
| osFile.open(fileLocation.c_str(), std::ios_base::out); |
| if ( osFile.good() ) |
| { |
| // osFile << "(echo \"" << aCondition.str() << "\")" << std::endl; |
| |
| InstanceOfData * aParam; |
| |
| std::size_t paramCount = paramVector.size(); |
| for( std::size_t offset = 0 ; offset < paramCount ; offset++ ) |
| { |
| aParam = paramVector[ offset ].to_ptr< InstanceOfData >(); |
| |
| osFile << "(declare-const " << aParam->getFullyQualifiedNameID() |
| << " "; |
| if( aParam->isTypedBoolean() ) |
| { |
| osFile << "Bool"; |
| } |
| else if( aParam->weaklyTypedInteger() || |
| aParam->isTypedEnum() ) |
| { |
| osFile << "Int"; |
| } |
| else if( aParam->weaklyTypedReal() ) |
| { |
| osFile << "Real"; |
| } |
| else |
| { |
| osFile << "Unknown"; |
| } |
| osFile << ")" << std::endl; |
| } |
| |
| osFile << "(assert " << ossCondition.str() << ")" << std::endl; |
| |
| osFile << "(get-model)" << std::endl; |
| |
| osFile.close(); |
| } |
| else |
| { |
| return( false ); |
| } |
| |
| return( true ); |
| } |
| |
| |
| |
| SolverDef::SATISFIABILITY_RING Z3Solver::from_smt_sat(const BF & aCondition) |
| { |
| SolverDef::SATISFIABILITY_RING satisfiability = SolverDef::SATISFIABLE; |
| |
| |
| return( satisfiability ); |
| } |
| |
| bool Z3Solver::from_smt_model(const BF & aCondition, |
| BFVector & dataVector, BFVector & valuesVector) |
| { |
| return( true ); |
| } |
| |
| |
| |
| void Z3Solver::to_smt(OutStream & os, |
| const BF & exprForm, BFVector & dataVector) const |
| { |
| AVM_OS_ASSERT_FATAL_NULL_SMART_POINTER_EXIT( exprForm ) << "expression !!!" |
| << SEND_EXIT; |
| |
| os << TAB; |
| |
| switch( exprForm.classKind() ) |
| { |
| case FORM_AVMCODE_KIND: |
| { |
| AvmCode * aCode = exprForm.to_ptr< AvmCode >(); |
| |
| os << '('; |
| std::string eoe = ""; |
| |
| switch( aCode->getAvmOpCode() ) |
| { |
| case AVM_OPCODE_AND: |
| { |
| os << "and"; |
| break; |
| } |
| case AVM_OPCODE_OR: |
| { |
| os << "or"; |
| break; |
| } |
| case AVM_OPCODE_NOT: |
| { |
| os << "not"; |
| break; |
| } |
| |
| case AVM_OPCODE_NEQ: |
| { |
| os << "(not"; |
| eoe = ")"; |
| break; |
| } |
| |
| case AVM_OPCODE_IFE: |
| { |
| os << "ite"; |
| break; |
| } |
| |
| case AVM_OPCODE_IF: |
| { |
| os << "if"; |
| break; |
| } |
| |
| default: |
| { |
| os << aCode->getOperator()->strSMT(); |
| break; |
| |
| } |
| } |
| |
| AvmCode::iterator it = aCode->begin(); |
| AvmCode::iterator endIt = aCode->end(); |
| for( ; it != endIt ; ++it ) |
| { |
| os << " "; |
| to_smt(os, *it, dataVector); |
| } |
| |
| os << eoe << ')'; |
| |
| break; |
| } |
| |
| case FORM_INSTANCE_DATA_KIND: |
| { |
| dataVector.add_union( exprForm ); |
| os << exprForm.to_ptr< InstanceOfData >()->getFullyQualifiedNameID(); |
| |
| break; |
| } |
| |
| |
| case FORM_BUILTIN_BOOLEAN_KIND: |
| case FORM_BUILTIN_INTEGER_KIND: |
| case FORM_BUILTIN_RATIONAL_KIND: |
| case FORM_BUILTIN_FLOAT_KIND: |
| { |
| os << exprForm.str(); |
| |
| break; |
| } |
| |
| default: |
| { |
| AVM_OS_FATAL_ERROR_EXIT |
| << "Unexpected BASEFORM KIND as expression << " |
| << exprForm.str() << " >> !!!" |
| << SEND_EXIT; |
| |
| os << exprForm.str(); |
| |
| break; |
| } |
| } |
| |
| os << EOL; |
| } |
| |
| |
| #else /* NOT _AVM_SOLVER_Z3_CPP_ ==> _AVM_SOLVER_Z3_C << default >> */ |
| |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| |
| |
| |
| /** |
| \brief Display a symbol in the given output stream. |
| */ |
| static void display_symbol(OutStream & os, Z3_context ctx, Z3_symbol s) |
| { |
| switch (Z3_get_symbol_kind(ctx, s)) { |
| case Z3_INT_SYMBOL: |
| os << "$" << Z3_get_symbol_int(ctx, s); |
| break; |
| case Z3_STRING_SYMBOL: |
| os << Z3_get_symbol_string(ctx, s); |
| break; |
| default: |
| AVM_OS_FATAL_ERROR_EXIT |
| << "unreachable code was reached !!!" |
| << SEND_EXIT; |
| break; |
| } |
| } |
| |
| /** |
| \brief Display the given type. |
| */ |
| static void display_sort(OutStream & os, Z3_context ctx, Z3_sort ty) |
| { |
| switch (Z3_get_sort_kind(ctx, ty)) { |
| case Z3_UNINTERPRETED_SORT: |
| display_symbol(os, ctx, Z3_get_sort_name(ctx, ty)); |
| break; |
| case Z3_BOOL_SORT: |
| os << "bool"; |
| break; |
| case Z3_INT_SORT: |
| os << "int"; |
| break; |
| case Z3_REAL_SORT: |
| os << "real"; |
| break; |
| case Z3_BV_SORT: |
| os << "bv" << Z3_get_bv_sort_size(ctx, ty); |
| break; |
| case Z3_ARRAY_SORT: |
| os << "["; |
| display_sort(os, ctx, Z3_get_array_sort_domain(ctx, ty)); |
| os << "->"; |
| display_sort(os, ctx, Z3_get_array_sort_range(ctx, ty)); |
| os << "]"; |
| break; |
| case Z3_DATATYPE_SORT: |
| if (Z3_get_datatype_sort_num_constructors(ctx, ty) != 1) |
| { |
| os << Z3_sort_to_string(ctx,ty); |
| break; |
| } |
| { |
| unsigned num_fields = Z3_get_tuple_sort_num_fields(ctx, ty); |
| unsigned i; |
| os << "("; |
| for (i = 0; i < num_fields; i++) { |
| Z3_func_decl field = Z3_get_tuple_sort_field_decl(ctx, ty, i); |
| if (i > 0) { |
| os << ", "; |
| } |
| display_sort(os, ctx, Z3_get_range(ctx, field)); |
| } |
| os << ")"; |
| break; |
| } |
| default: |
| os << "unknown["; |
| display_symbol(os, ctx, Z3_get_sort_name(ctx, ty)); |
| os << "]"; |
| break; |
| } |
| } |
| |
| /** |
| \brief Custom ast pretty printer. |
| |
| This function demonstrates how to use the API to navigate terms. |
| */ |
| static void display_ast(OutStream & os, Z3_context ctx, Z3_ast v) |
| { |
| switch (Z3_get_ast_kind(ctx, v)) { |
| case Z3_NUMERAL_AST: { |
| Z3_sort t; |
| os << Z3_get_numeral_string(ctx, v); |
| t = Z3_get_sort(ctx, v); |
| os << ":"; |
| display_sort(os, ctx, t); |
| break; |
| } |
| case Z3_APP_AST: { |
| Z3_app app = Z3_to_app(ctx, v); |
| unsigned num_fields = Z3_get_app_num_args(ctx, app); |
| Z3_func_decl d = Z3_get_app_decl(ctx, app); |
| os << Z3_func_decl_to_string(ctx, d); |
| if (num_fields > 0) { |
| os << "["; |
| display_ast(os, ctx, Z3_get_app_arg(ctx, app, 0)); |
| for (unsigned i = 1; i < num_fields; i++) { |
| os << ", "; |
| display_ast(os, ctx, Z3_get_app_arg(ctx, app, i)); |
| } |
| os << "]"; |
| } |
| break; |
| } |
| case Z3_QUANTIFIER_AST: { |
| os << "quantifier"; |
| break; |
| } |
| default: { |
| os << "#unknown"; |
| break; |
| } |
| } |
| } |
| |
| /** |
| \brief Custom function interpretations pretty printer. |
| */ |
| static void display_function_interpretations( |
| OutStream & os, Z3_context ctx, Z3_model model) |
| { |
| unsigned num_functions, i; |
| |
| os << "function interpretations:" << std::endl; |
| |
| num_functions = Z3_get_model_num_funcs(ctx, model); |
| for (i = 0; i < num_functions; i++) { |
| Z3_func_decl fdecl; |
| Z3_symbol name; |
| Z3_ast func_else; |
| unsigned num_entries, j; |
| |
| fdecl = Z3_get_model_func_decl(ctx, model, i); |
| name = Z3_get_decl_name(ctx, fdecl); |
| display_symbol(os, ctx, name); |
| os << " = {"; |
| num_entries = Z3_get_model_func_num_entries(ctx, model, i); |
| for (j = 0; j < num_entries; j++) { |
| unsigned num_args, k; |
| if (j > 0) { |
| os << ", "; |
| } |
| num_args = Z3_get_model_func_entry_num_args(ctx, model, i, j); |
| os << "("; |
| for (k = 0; k < num_args; k++) { |
| if (k > 0) { |
| os << ", "; |
| } |
| display_ast(os, ctx, Z3_get_model_func_entry_arg(ctx, model, i, j, k)); |
| } |
| os << "|->"; |
| display_ast(os, ctx, Z3_get_model_func_entry_value(ctx, model, i, j)); |
| os << ")"; |
| } |
| if (num_entries > 0) { |
| os << ", "; |
| } |
| os << "(else|->"; |
| func_else = Z3_get_model_func_else(ctx, model, i); |
| display_ast(os, ctx, func_else); |
| os << ")}" << std::endl; |
| } |
| } |
| |
| /** |
| \brief Custom model pretty printer. |
| */ |
| static void display_model(OutStream & os, Z3_context ctx, Z3_model model) |
| { |
| unsigned num_constants; |
| unsigned i; |
| |
| num_constants = Z3_get_model_num_constants(ctx, model); |
| for (i = 0; i < num_constants; i++) { |
| Z3_symbol name; |
| Z3_func_decl cnst = Z3_get_model_constant(ctx, model, i); |
| Z3_ast a, v; |
| name = Z3_get_decl_name(ctx, cnst); |
| display_symbol(os, ctx, name); |
| os << " = "; |
| a = Z3_mk_app(ctx, cnst, 0, 0); |
| v = a; |
| Z3_bool ok = Z3_eval(ctx, model, a, &v); |
| if( ok == Z3_TRUE ) |
| { |
| display_ast(os, ctx, v); |
| os << std::endl; |
| } |
| } |
| display_function_interpretations(os, ctx, model); |
| } |
| |
| |
| |
| |
| |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| //////////////////////////////////////////////////////////////////////////////// |
| |
| |
| |
| /** |
| * CONFIGURE |
| */ |
| bool Z3Solver::configure( |
| Configuration & aConfiguration, WObject * wfFilterObject, |
| ListOfPairMachineData & listOfSelectedVariable) |
| { |
| if( not base_this_type::configure( |
| aConfiguration, wfFilterObject, listOfSelectedVariable) ) |
| { |
| return( false ); |
| } |
| |
| return( true ); |
| } |
| |
| |
| |
| /** |
| * CREATE - DESTROY |
| * ValidityChecker |
| */ |
| |
| /** |
| \brief Simpler error handler. |
| */ |
| void error_handler(Z3_error_code e) |
| { |
| AVM_OS_EXIT( FAILED ) |
| << "Z3Solver:> Incorrect use of the solver, error code << " |
| << e << " >>" |
| << SEND_EXIT; |
| } |
| |
| |
| bool Z3Solver::createChecker() |
| { |
| CFG = Z3_mk_config(); |
| |
| Z3_set_param_value(CFG, "MODEL", "true"); |
| |
| CTX = Z3_mk_context(CFG); |
| |
| // Z3_set_error_handler(error_handler); |
| |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| ++SOLVER_SESSION_ID; |
| AVM_IF_DEBUG_LEVEL_GTE_HIGH |
| mLogFolderLocation = OSS() << VFS::ProjectLogPath << "/z3/"; |
| |
| if ( not VFS::checkWritingFolder(mLogFolderLocation) ) |
| { |
| AVM_OS_LOG << " Z3Solver::createChecker :> Error: The folder " |
| << "`" << mLogFolderLocation << "' " |
| << "---> doesn't exist or is not writable !!!" |
| << std::endl << std::endl; |
| return( false ); |
| } |
| |
| // std::string fileLocation = OSS << mLogFolderLocation |
| // << "z3_log_" << SOLVER_SESSION_ID << ".z3"; |
| // Z3_open_log( fileLocation.c_str() ); |
| // |
| // fileLocation = OSS << mLogFolderLocation |
| // << "z3_trace_" << SOLVER_SESSION_ID << ".z3"; |
| // Z3_trace_to_file( CTX , fileLocation.c_str() ); |
| AVM_ENDIF_DEBUG_LEVEL_GTE_HIGH |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| |
| |
| SMT_TYPE_BOOL = Z3_mk_bool_sort(CTX); |
| SMT_TYPE_INT = Z3_mk_int_sort(CTX); |
| SMT_TYPE_REAL = Z3_mk_real_sort(CTX); |
| |
| SMT_CST_BOOL_TRUE = Z3_mk_true(CTX); |
| SMT_CST_BOOL_FALSE = Z3_mk_false(CTX); |
| |
| SMT_CST_INT_ZERO = Z3_mk_int(CTX, 0, SMT_TYPE_INT); |
| SMT_CST_INT_ONE = Z3_mk_int(CTX, 1, SMT_TYPE_INT); |
| |
| resetTable(); |
| |
| return( true ); |
| } |
| |
| |
| bool Z3Solver::destroyChecker() |
| { |
| resetTable(); |
| |
| SMT_TYPE_BOOL = NULL; |
| SMT_TYPE_INT = NULL; |
| SMT_TYPE_BV32 = NULL; |
| SMT_TYPE_BV64 = NULL; |
| SMT_TYPE_REAL = NULL; |
| |
| SMT_CST_BOOL_TRUE = NULL; |
| SMT_CST_BOOL_FALSE = NULL; |
| |
| SMT_CST_INT_ZERO = NULL; |
| SMT_CST_INT_ONE = NULL; |
| |
| // Z3_close_log(); |
| // Z3_trace_off( CTX ); |
| |
| if( CFG != NULL ) |
| { |
| Z3_del_config(CFG); |
| CFG = NULL; |
| } |
| |
| if( CTX != NULL ) |
| { |
| Z3_del_context(CTX); |
| |
| CTX = NULL; |
| } |
| |
| return( true ); |
| } |
| |
| bool Z3Solver::resetTable() |
| { |
| base_this_type::resetTable(); |
| |
| mTableOfParameterDecl.append( NULL ); |
| |
| mTableOfParameterExpr.append( NULL ); |
| |
| return( true ); |
| } |
| |
| |
| |
| /** |
| * PROVER |
| */ |
| bool Z3Solver::isSubSet( |
| const ExecutionContext & newEC, const ExecutionContext & oldEC) |
| { |
| return( true ); |
| } |
| |
| bool Z3Solver::isEqualSet( |
| const ExecutionContext & newEC, const ExecutionContext & oldEC) |
| { |
| return( true ); |
| } |
| |
| SolverDef::SATISFIABILITY_RING Z3Solver::isSatisfiable(const BF & aCondition) |
| { |
| SolverDef::SATISFIABILITY_RING satisfiability = SolverDef::SATISFIABLE; |
| |
| createChecker(); |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| AVM_OS_TRACE << "Z3Solver::isSatisfiable(...) " |
| ":" << SOLVER_SESSION_ID << ">" << std::endl |
| << "\t" << aCondition.str() << std::endl; |
| |
| // trace to file |
| AVM_IF_DEBUG_LEVEL_GTE_HIGH |
| smt_check_sat(aCondition); |
| AVM_ENDIF_DEBUG_LEVEL_GTE_HIGH |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| |
| Z3_ast z3Condition = from_baseform(aCondition); |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| AVM_OS_TRACE << "Z3Condition :" << SOLVER_SESSION_ID << ">" |
| << std::endl; |
| AVM_IF_DEBUG_LEVEL_GTE_HIGH |
| AVM_OS_TRACE << "\t"; |
| display_ast(AVM_OS_TRACE, CTX, z3Condition); |
| AVM_OS_TRACE << std::endl; |
| AVM_ENDIF_DEBUG_LEVEL_GTE_HIGH |
| AVM_OS_TRACE << "\t" << Z3_ast_to_string(CTX, z3Condition) << std::endl; |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( HIGH , SMT_SOLVING ) |
| AVM_OS_TRACE << "Z3::CTX :" << SOLVER_SESSION_ID << ">" << std::endl |
| << Z3_context_to_string(CTX) << std::endl; |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( HIGH , SMT_SOLVING ) |
| |
| if( z3Condition != NULL ) |
| { |
| Z3_assert_cnstr(CTX, z3Condition); |
| |
| switch( Z3_check(CTX) ) |
| { |
| case Z3_L_TRUE: |
| { |
| satisfiability = SolverDef::SATISFIABLE; |
| break; |
| } |
| |
| case Z3_L_FALSE: |
| { |
| satisfiability = SolverDef::UNSATISFIABLE; |
| break; |
| } |
| |
| case Z3_L_UNDEF: |
| { |
| satisfiability = SolverDef::UNKNOWN_SAT; |
| break; |
| } |
| |
| default: |
| { |
| satisfiability = SolverDef::ABORT_SAT; |
| break; |
| } |
| } |
| } |
| |
| destroyChecker(); |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| AVM_OS_TRACE << "result :" << SOLVER_SESSION_ID << "> " |
| << SolverDef::strSatisfiability(satisfiability) << std::endl; |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| |
| return( satisfiability ); |
| } |
| |
| |
| /** |
| * SOLVER |
| */ |
| bool Z3Solver::solveImpl(const BF & aCondition, |
| BFVector & dataVector, BFVector & valuesVector) |
| { |
| SolverDef::SATISFIABILITY_RING satisfiability = SolverDef::SATISFIABLE; |
| |
| createChecker(); |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| AVM_OS_TRACE << "Z3Solver::solve(...) " |
| ":" << SOLVER_SESSION_ID << ">" << std::endl |
| << "\t" << aCondition.str() << std::endl; |
| |
| // trace to file |
| smt_check_model(aCondition, dataVector, valuesVector); |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| |
| Z3_ast z3Condition = from_baseform(aCondition); |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| AVM_OS_TRACE << "Z3Condition :" << SOLVER_SESSION_ID << ">" |
| << std::endl; |
| AVM_IF_DEBUG_LEVEL_GTE_HIGH |
| AVM_OS_TRACE << "\t"; |
| display_ast(AVM_OS_TRACE, CTX, z3Condition); |
| AVM_OS_TRACE << std::endl; |
| AVM_ENDIF_DEBUG_LEVEL_GTE_HIGH |
| AVM_OS_TRACE << "\t" << Z3_ast_to_string(CTX, z3Condition) << std::endl; |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( HIGH , SMT_SOLVING ) |
| AVM_OS_TRACE << "Z3::CTX :" << SOLVER_SESSION_ID << ">" << std::endl |
| << Z3_context_to_string(CTX) << std::endl; |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( HIGH , SMT_SOLVING ) |
| |
| if( z3Condition != NULL ) |
| { |
| Z3_assert_cnstr(CTX, z3Condition); |
| |
| Z3_model model = NULL; |
| |
| switch( Z3_check_and_get_model(CTX, &model) ) |
| { |
| case Z3_L_TRUE: |
| { |
| satisfiability = SolverDef::SATISFIABLE; |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| AVM_OS_TRACE << "Z3Model sat:" << SOLVER_SESSION_ID << ">" << std::endl |
| << Z3_model_to_string(CTX, model) << std::endl; |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| |
| unsigned num_constants = Z3_get_model_num_constants(CTX, model); |
| for( unsigned i = 0 ; i < num_constants ; i++ ) |
| { |
| Z3_func_decl cnst = Z3_get_model_constant(CTX, model, i); |
| |
| Z3_symbol symbol = Z3_get_decl_name(CTX, cnst); |
| |
| int offset = mTableOfParameterDecl.find(symbol); |
| if( offset >= 0 ) |
| { |
| dataVector.append( mTableOfParameterInstance[offset] ); |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| display_symbol(AVM_OS_TRACE, CTX, symbol); |
| AVM_OS_TRACE << " := "; |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| |
| Z3_ast app = Z3_mk_app(CTX, cnst, 0, 0); |
| |
| Z3_ast value = app; |
| |
| Z3_bool ok = Z3_eval(CTX, model, app, &value); |
| |
| switch( ok ) |
| { |
| case Z3_L_TRUE: |
| { |
| BF bfVal = to_baseform(model, value); |
| |
| valuesVector.append( bfVal.valid() ? |
| bfVal : dataVector.back() ); |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| display_ast(AVM_OS_TRACE, CTX, value); |
| AVM_OS_TRACE << std::endl; |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| break; |
| } |
| case Z3_L_FALSE: |
| case Z3_L_UNDEF: |
| default: |
| { |
| valuesVector.append( BF::REF_NULL ); |
| |
| AVM_OS_FATAL_ERROR_EXIT |
| << "Z3Solver::solve :> " |
| "failed to Z3_eval << " |
| << Z3_ast_to_string(CTX, app) |
| << " >> !!!" |
| << SEND_EXIT; |
| |
| break; |
| } |
| } |
| } |
| else |
| { |
| AVM_OS_FATAL_ERROR_EXIT |
| << "Z3Solver::solve :> " |
| "unfound parameter instance for Z3 symbol << " |
| << Z3_get_symbol_string(CTX, symbol) |
| << " >> !!!" |
| << SEND_EXIT; |
| } |
| } |
| |
| |
| break; |
| } |
| |
| case Z3_L_FALSE: |
| { |
| satisfiability = SolverDef::UNSATISFIABLE; |
| break; |
| } |
| |
| case Z3_L_UNDEF: |
| { |
| satisfiability = SolverDef::UNKNOWN_SAT; |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| AVM_OS_TRACE << "Z3Model undef:" << SOLVER_SESSION_ID << ">" |
| << std::endl; |
| AVM_OS_TRACE << Z3_model_to_string(CTX, model) << std::endl; |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| |
| break; |
| } |
| |
| default: |
| { |
| satisfiability = SolverDef::ABORT_SAT; |
| break; |
| } |
| } |
| |
| if( model != NULL ) |
| { |
| Z3_del_model(CTX, model); |
| } |
| |
| } |
| |
| destroyChecker(); |
| |
| AVM_IF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| AVM_OS_TRACE << "solve :" << SOLVER_SESSION_ID << "> " |
| << SolverDef::strSatisfiability(satisfiability) << std::endl; |
| AVM_ENDIF_DEBUG_LEVEL_FLAG( MEDIUM , SMT_SOLVING ) |
| |
| return( satisfiability == SolverDef::SATISFIABLE ); |
| } |
| |
| |
| |
| /** |
| * TOOLS |
| */ |
| |
| Z3_sort Z3Solver::getZ3Type(BaseTypeSpecifier * bts) |
| { |
| if( bts->isTypedBoolean() ) |
| { |
| return( SMT_TYPE_BOOL ); |
| } |
| else if( bts->isTypedEnum() ) |
| { |
| return( SMT_TYPE_INT ); |
| // TODO Attention : il faudrait rajouter les contraintes |
| // d'intervalle pour le type énuméré |
| } |
| else if( bts->weaklyTypedInteger() ) |
| { |
| return( SMT_TYPE_INT ); |
| } |
| else if( bts->weaklyTypedReal() ) |
| { |
| return( SMT_TYPE_REAL ); |
| } |
| |
| else if( bts->isTypedMachine() ) |
| { |
| // TODO:> Consolidation après TEST |
| return( SMT_TYPE_INT ); |
| } |
| |
| return( SMT_TYPE_REAL ); |
| } |
| |
| |
| Z3_ast Z3Solver::getParameterExpr(const BF & bfParameter) |
| { |
| InstanceOfData * aParameter = bfParameter.to_ptr< InstanceOfData >(); |
| |
| if( aParameter->getMark() == 0 ) |
| { |
| aParameter->setMark( mTableOfParameterInstance.size() ); |
| mTableOfParameterInstance.append( bfParameter ); |
| |
| mTableOfParameterDecl.push_back( Z3_mk_string_symbol( CTX, |
| // ( OSS << "P_" << aParameter->getMark() ).c_str() ) ); |
| aParameter->getNameID().c_str() ) ); |
| |
| mTableOfParameterExpr.push_back( Z3_mk_const( CTX, |
| mTableOfParameterDecl.last(), |
| getZ3Type(aParameter->referedTypeSpecifier())) ); |
| } |
| |
| return( mTableOfParameterExpr.at( aParameter->getMark() ) ); |
| } |
| |
| |
| |
| |
| Z3_ast Z3Solver::getVariableExpr(InstanceOfData * aVar, std::size_t varID) |
| { |
| if( mTableOfVariableExpr.size() <= varID ) |
| { |
| mTableOfVariableDecl.push_back( Z3_mk_string_symbol( CTX, |
| // ( OSS << "V_" << varID ).c_str() ) ); |
| aVar->getNameID().c_str() ) ); |
| |
| mTableOfVariableExpr.push_back( Z3_mk_const( CTX, |
| mTableOfVariableDecl.last(), |
| getZ3Type(aVar->getTypeSpecifier()) ) ); |
| } |
| |
| return( mTableOfVariableExpr.at( varID ) ); |
| } |
| |
| |
| |
| Z3_ast Z3Solver::safe_from_baseform(const BF & exprForm, |
| BaseTypeSpecifier * typeSpecifier) |
| { |
| Z3_ast e = NULL; |
| |
| try |
| { |
| if( (e = from_baseform(exprForm, typeSpecifier)) == NULL ) |
| { |
| AVM_OS_WARN << std::endl << REPEAT("********", 10) << std::endl |
| << "\tZ3Solver::safe_from_baseform< unknown::error :" |
| << SOLVER_SESSION_ID << ">" << std::endl |
| << REPEAT("--------", 10) << std::endl |
| << "\tFailed to CONVERT sep::fml::expression to Z3::Expr:>" << std::endl |
| << "\t " << exprForm.str() << std::endl |
| << REPEAT("********", 10) << std::endl; |
| |
| destroyChecker(); |
| } |
| } |
| catch ( ... ) |
| { |
| AVM_OS_WARN << std::endl << REPEAT("********", 10) << std::endl |
| << "\tZ3Solver::safe_from_baseform< unknown::exception :" |
| << SOLVER_SESSION_ID << ">" << std::endl |
| << REPEAT("--------", 10) << std::endl |
| << "\tFailed to CONVERT sep::fml::expression to Z3::Expr:>" << std::endl |
| << "\t " << exprForm.str() << std::endl |
| << REPEAT("********", 10) << std::endl; |
| |
| destroyChecker(); |
| } |
| |
| return( e ); |
| } |
| |
| |
| |
| Z3_ast Z3Solver::from_baseform(const BF & exprForm, |
| BaseTypeSpecifier * typeSpecifier) |
| { |
| AVM_OS_ASSERT_FATAL_NULL_SMART_POINTER_EXIT( exprForm ) << "expression !!!" |
| << SEND_EXIT; |
| |
| switch( exprForm.classKind() ) |
| { |
| case FORM_AVMCODE_KIND: |
| { |
| AvmCode * aCode = exprForm.to_ptr< AvmCode >(); |
| |
| typeSpecifier = TypeManager::UNIVERSAL; |
| |
| switch( aCode->getAvmOpCode() ) |
| { |
| // COMPARISON OPERATION |
| case AVM_OPCODE_EQ: |
| { |
| return( Z3_mk_eq( CTX, |
| from_baseform(aCode->first() , typeSpecifier), |
| from_baseform(aCode->second(), typeSpecifier) ) ); |
| } |
| |
| case AVM_OPCODE_NEQ: |
| { |
| return( Z3_mk_not( CTX, Z3_mk_eq( CTX, |
| from_baseform(aCode->first() , typeSpecifier), |
| from_baseform(aCode->second(), typeSpecifier) ) ) ); |
| |
| // ARGS arg( 2 ); |
| // |
| // arg.next( from_baseform(aCode->first() , typeSpecifier) ); |
| // arg.next( from_baseform(aCode->second(), typeSpecifier) ); |
| // |
| // return( Z3_mk_distinct(CTX, 2, arg->table) ); |
| } |
| |
| case AVM_OPCODE_LT: |
| { |
| return( Z3_mk_lt( CTX, |
| from_baseform(aCode->first() , typeSpecifier), |
| from_baseform(aCode->second(), typeSpecifier) ) ); |
| } |
| |
| case AVM_OPCODE_LTE: |
| { |
| return( Z3_mk_le( CTX, |
| from_baseform(aCode->first() , typeSpecifier), |
| from_baseform(aCode->second(), typeSpecifier) ) ); |
| } |
| |
| case AVM_OPCODE_GT: |
| { |
| return( Z3_mk_gt( CTX, |
| from_baseform(aCode->first() , typeSpecifier), |
| from_baseform(aCode->second(), typeSpecifier) ) ); |
| } |
| |
| case AVM_OPCODE_GTE: |
| { |
| return( Z3_mk_ge( CTX, |
| from_baseform(aCode->first() , typeSpecifier), |
| from_baseform(aCode->second(), typeSpecifier) ) ); |
| } |
| |
| |
| // LOGICAL OPERATION |
| case AVM_OPCODE_NOT: |
| { |
| return( Z3_mk_not( CTX, |
| from_baseform(aCode->first() , typeSpecifier)) ); |
| } |
| |
| case AVM_OPCODE_AND: |
| { |
| ARGS arg( aCode->size() ); |
| |
| AvmCode::iterator it = aCode->begin(); |
| for( ; arg.hasNext() ; ++it ) |
| { |
| arg.next( from_baseform(*it, typeSpecifier) ); |
| } |
| |
| return( Z3_mk_and(CTX, arg->count, arg->table) ); |
| } |
| |
| case AVM_OPCODE_NAND: |
| { |
| ARGS arg( aCode->size() ); |
| |
| AvmCode::iterator it = aCode->begin(); |
| for( ; arg.hasNext() ; ++it ) |
| { |
| arg.next( from_baseform(*it, typeSpecifier) ); |
| } |
| |
| return( Z3_mk_not( CTX, Z3_mk_and(CTX, arg->count, arg->table) ) ); |
| } |
| |
| // case AVM_OPCODE_XAND: |
| // { |
| // ARGS arg( 2 ); |
| // |
| // arg.next( Z3_mk_not( CTX, |
| // from_baseform(aCode->first() , typeSpecifier)) ); |
| // arg.next( from_baseform(aCode->second(), typeSpecifier) ); |
| // |
| // return( Z3_mk_and(CTX, arg->table, 2) ); |
| // |
| // return( mVC->orExpr( |
| // mVC->andExpr(from_baseform(aCode->first(), typeSpecifier), |
| // from_baseform(aCode->second(), typeSpecifier)), |
| // mVC->andExpr(mVC->notExpr(from_baseform(aCode->first(), typeSpecifier)), |
| // mVC->notExpr(from_baseform(aCode->second(), typeSpecifier))) ) ); |
| // } |
| |
| |
| case AVM_OPCODE_OR: |
| { |
| ARGS arg( aCode->size() ); |
| |
| AvmCode::iterator it = aCode->begin(); |
| for( ; arg.hasNext() ; ++it ) |
| { |
| arg.next( from_baseform(*it, typeSpecifier) ); |
| } |
| |
| return( Z3_mk_or(CTX, arg->count, arg->table) ); |
| } |
| |
| case AVM_OPCODE_NOR: |
| { |
| ARGS arg( aCode->size() ); |
| |
| AvmCode::iterator it = aCode->begin(); |
| for( ; arg.hasNext() ; ++it ) |
| { |
| arg.next( from_baseform(*it, typeSpecifier) ); |
| } |
| |
| return( Z3_mk_not( CTX, Z3_mk_or(CTX, arg->count, arg->table) ) ); |
| } |
| |
| // case AVM_OPCODE_BAND: |
| // { |
| // return( Z3_mk_bv_and( CTX, |
| // from_baseform(aCode->first(), typeSpecifier), |
| // from_baseform(aCode->second(), typeSpecifier) ) ); |
| // } |
| // |
| // case AVM_OPCODE_BOR: |
| // { |
| // return( Z3_mk_bv_or( CTX, |
| // from_baseform(aCode->first(), typeSpecifier), |
| // from_baseform(aCode->second(), typeSpecifier) ) ); |
| // } |
| // |
| // case AVM_OPCODE_LSHIFT: |
| // { |
| // if( aCode->second().isInteger() ) |
| // { |
| // return( Z3_mk_bv_shift_left0( CTX, |
| // from_baseform(aCode->first(), typeSpecifier), |
| // aCode->second().toInteger()) ); |
| // |
| // } |
| // else |
| // { |
| // AVM_OS_FATAL_ERROR_EXIT |
| // << "Unexpected second argument for " |
| // "newFixedLeftShiftExpr !!!\n" |
| // << aCode->toString( AVM_TAB1_INDENT ) |
| // << SEND_EXIT; |
| // |
| // return( NULL ); |
| // } |
| // } |
| // |
| // case AVM_OPCODE_RSHIFT: |
| // { |
| // if( aCode->second().isInteger() ) |
| // { |
| // return( Z3_mk_bv_shift_right0( CTX, |
| // from_baseform(aCode->first(), typeSpecifier), |
| // aCode->second().toInteger()) ); |
| // |
| // } |
| // else |
| // { |
| // AVM_OS_FATAL_ERROR_EXIT |
| // << "Unexpected second argument for " |
| // "newFixedRightShiftExpr !!!\n" |
| // << aCode->toString( AVM_TAB1_INDENT ) |
| // << SEND_EXIT; |
| // |
| // return( NULL ); |
| // } |
| // } |
| |
| case AVM_OPCODE_XOR: |
| { |
| return( Z3_mk_xor( CTX, |
| from_baseform(aCode->first() , typeSpecifier), |
| from_baseform(aCode->second(), typeSpecifier) ) ); |
| } |
| |
| case AVM_OPCODE_XNOR: |
| { |
| return( Z3_mk_not( CTX, Z3_mk_xor( CTX, |
| from_baseform(aCode->first() , typeSpecifier), |
| from_baseform(aCode->second(), typeSpecifier) ) ) ); |
| } |
| |
| |
| // ARITHMETIC OPERATION |
| case AVM_OPCODE_PLUS: |
| { |
| ARGS arg( aCode->size() ); |
| |
| AvmCode::iterator it = aCode->begin(); |
| for( ; arg.hasNext() ; ++it ) |
| { |
| arg.next( from_baseform(*it, typeSpecifier) ); |
| } |
| |
| return( Z3_mk_add(CTX, arg->count, arg->table) ); |
| } |
| |
| case AVM_OPCODE_UMINUS: |
| { |
| return( Z3_mk_unary_minus(CTX, |
| from_baseform(aCode->first(), typeSpecifier)) ); |
| } |
| |
| case AVM_OPCODE_MINUS: |
| { |
| ARGS arg( aCode->size() ); |
| |
| AvmCode::iterator it = aCode->begin(); |
| for( ; arg.hasNext() ; ++it ) |
| { |
| arg.next( from_baseform(*it, typeSpecifier) ); |
| } |
| |
| return( Z3_mk_sub(CTX, arg->count, arg->table) ); |
| } |
| |
| case AVM_OPCODE_MULT: |
| { |
| ARGS arg( aCode->size() ); |
| |
| AvmCode::iterator it = aCode->begin(); |
| for( ; arg.hasNext() ; ++it ) |
| { |
| arg.next( from_baseform(*it, typeSpecifier) ); |
| } |
| |
| return( Z3_mk_mul(CTX, arg->count, arg->table) ); |
| } |
| |
| case AVM_OPCODE_DIV: |
| { |
| return( Z3_mk_div( CTX, |
| from_baseform(aCode->first() , typeSpecifier), |
| from_baseform(aCode->second(), typeSpecifier) ) ); |
| } |
| |
| case AVM_OPCODE_POW: |
| { |
| if( ExpressionFactory::isPosInteger(aCode->second()) ) |
| { |
| // return( Z3_mk_power( CTX, |
| // from_baseform(aCode->first() , typeSpecifier), |
| // from_baseform(aCode->second(), typeSpecifier) ) ); |
| |
| avm_uinteger_t power = |
| ExpressionFactory::toUInteger(aCode->second()); |
| |
| ARGS arg( power ); |
| |
| arg.next( from_baseform(aCode->first()) ); |
| |
| while( arg.hasNext() ) |
| { |
| arg.next( arg[ 0 ] ); |
| } |
| |
| return( Z3_mk_mul(CTX, arg->count, arg->table) ); |
| } |
| else |
| { |
| AVM_OS_FATAL_ERROR_EXIT |
| << "Z3Solver::from_baseform:> Unsupported " |
| "expression Operator << AVM_OPCODE_POW >> !!!" |
| << SEND_EXIT; |
| |
| return( NULL ); |
| } |
| } |
| |
| case AVM_OPCODE_MOD: |
| { |
| return( Z3_mk_mod( CTX, |
| from_baseform(aCode->first() , typeSpecifier), |
| from_baseform(aCode->second(), typeSpecifier) ) ); |
| } |
| |
| |
| default: |
| { |
| AVM_OS_FATAL_ERROR_EXIT |
| << "Z3Solver::from_baseform:> Unexpected " |
| "BASEFORM KIND for execution !!!\n" |
| << aCode->toString( AVM_TAB1_INDENT ) |
| << SEND_EXIT; |
| |
| return( NULL ); |
| } |
| } |
| |
| break; |
| } |
| |
| case FORM_INSTANCE_DATA_KIND: |
| { |
| return( getParameterExpr( exprForm ) ); |
| } |
| |
| case FORM_BUILTIN_BOOLEAN_KIND: |
| { |
| if( exprForm.to_ptr< Boolean >()->getValue() ) |
| { |
| return( ((typeSpecifier != NULL) && typeSpecifier->isTypedBoolean()) ? |
| SMT_CST_BOOL_TRUE : SMT_CST_INT_ONE ); |
| } |
| else |
| { |
| return( ((typeSpecifier != NULL) && typeSpecifier->isTypedBoolean()) ? |
| SMT_CST_BOOL_FALSE : SMT_CST_INT_ZERO ); |
| } |
| } |
| |
| |
| case FORM_BUILTIN_INTEGER_KIND: |
| { |
| if( (typeSpecifier != NULL) && typeSpecifier->isTypedBoolean() ) |
| { |
| return( exprForm.to_ptr< Integer >()->isZero() ? |
| SMT_CST_BOOL_FALSE : SMT_CST_BOOL_TRUE ); |
| } |
| else |
| { |
| #if defined( _AVM_BUILTIN_NUMERIC_GMP_ ) |
| |
| return( Z3_mk_int64(CTX, |
| exprForm.to_ptr< Integer >()->toInteger(), |
| SMT_TYPE_INT) ); |
| |
| #else |
| |
| return( Z3_mk_int64(CTX, |
| exprForm.to_ptr< Integer >()->toInteger(), |
| SMT_TYPE_INT) ); |
| |
| #endif /* _AVM_BUILTIN_NUMERIC_GMP_ */ |
| } |
| |
| // return( Z3_mk_numeral(CTX, |
| // exprForm.to_ptr< Integer >()->str().c_str(), |
| // SMT_TYPE_INT) ); |
| } |
| |
| case FORM_BUILTIN_RATIONAL_KIND: |
| { |
| if( (typeSpecifier != NULL) && typeSpecifier->isTypedBoolean() ) |
| { |
| return( exprForm.to_ptr< Rational >()->isZero() ? |
| SMT_CST_BOOL_FALSE : SMT_CST_BOOL_TRUE ); |
| } |
| else |
| { |
| #if defined( _AVM_BUILTIN_NUMERIC_GMP_ ) |
| |
| return( Z3_mk_real(CTX, |
| exprForm.to_ptr< Rational >()->toNumerator(), |
| exprForm.to_ptr< Rational >()->toDenominator() ) ); |
| |
| #else |
| |
| return( Z3_mk_real(CTX, |
| exprForm.to_ptr< Rational >()->toNumerator(), |
| exprForm.to_ptr< Rational >()->toDenominator() ) ); |
| |
| #endif /* _AVM_BUILTIN_NUMERIC_GMP_ */ |
| } |
| |
| // return( Z3_mk_numeral( CTX, |
| // exprForm.to_ptr< Rational >()->str().c_str(), |
| // SMT_TYPE_REAL) ); |
| } |
| |
| case FORM_BUILTIN_FLOAT_KIND: |
| { |
| if( (typeSpecifier != NULL) && typeSpecifier->isTypedBoolean() ) |
| { |
| return( exprForm.to_ptr< Float >()->isZero() ? |
| SMT_CST_BOOL_FALSE : SMT_CST_BOOL_TRUE ); |
| } |
| else |
| { |
| #if defined( _AVM_BUILTIN_NUMERIC_GMP_ ) |
| |
| return( Z3_mk_numeral(CTX, |
| exprForm.to_ptr< Float >()->str().c_str(), |
| SMT_TYPE_REAL) ); |
| |
| #else |
| |
| return( Z3_mk_numeral(CTX, |
| exprForm.to_ptr< Float >()->str().c_str(), |
| SMT_TYPE_REAL) ); |
| |
| #endif /* _AVM_BUILTIN_NUMERIC_GMP_ */ |
| } |
| } |
| |
| |
| case FORM_RUNTIME_ID_KIND: |
| { |
| return( Z3_mk_int(CTX, exprForm.bfRID().getRid(), SMT_TYPE_INT) ); |
| } |
| |
| default: |
| { |
| AVM_OS_FATAL_ERROR_EXIT |
| << "Z3Solver::from_baseform:> Unexpected BASEFORM KIND << " |
| << exprForm.classKindName() << " >> as expression << " |
| << exprForm.str() << " >> !!!" |
| << SEND_EXIT; |
| |
| return( NULL ); |
| } |
| } |
| |
| AVM_OS_FATAL_ERROR_EXIT |
| << "Z3Solver::from_baseform ERROR !!!" |
| << SEND_EXIT; |
| |
| return( NULL ); |
| } |
| |
| |
| BF Z3Solver::to_baseform(Z3_model model, Z3_ast z3Form) |
| { |
| switch( Z3_get_ast_kind(CTX, z3Form) ) |
| { |
| case Z3_NUMERAL_AST: |
| { |
| Z3_sort type = Z3_get_sort(CTX, z3Form); |
| |
| switch( Z3_get_sort_kind(CTX, type) ) |
| { |
| case Z3_BOOL_SORT: |
| { |
| switch( Z3_get_bool_value(CTX, z3Form) ) |
| { |
| case Z3_L_TRUE: |
| { |
| return( ExpressionConstructor::newBoolean( true ) ); |
| } |
| case Z3_L_FALSE: |
| { |
| return( ExpressionConstructor::newBoolean( false ) ); |
| } |
| case Z3_L_UNDEF: |
| default: |
| { |
| return( ExpressionConstructor::newBoolean( |
| Z3_get_numeral_string(CTX, z3Form)) ); |
| } |
| } |
| } |
| case Z3_INT_SORT: |
| { |
| { |
| int val; |
| if( Z3_get_numeral_int(CTX, z3Form, &val) == Z3_L_TRUE ) |
| { |
| return( ExpressionConstructor::newInteger( |
| static_cast< avm_integer_t >( val ) ) ); |
| } |
| } |
| { |
| unsigned val; |
| if( Z3_get_numeral_uint(CTX, z3Form, &val) == Z3_L_TRUE ) |
| { |
| return( ExpressionConstructor::newUInteger( |
| static_cast< avm_uinteger_t >( val ) ) ); |
| } |
| } |
| { |
| __int64 val; |
| if( Z3_get_numeral_int64(CTX, z3Form, &val) == Z3_L_TRUE ) |
| { |
| return( ExpressionConstructor::newInteger( |
| static_cast< avm_integer_t >( val ) ) ); |
| } |
| } |
| { |
| unsigned __int64 val; |
| if( Z3_get_numeral_uint64(CTX, z3Form, &val) == Z3_L_TRUE ) |
| { |
| return( ExpressionConstructor::newUInteger( |
| static_cast< avm_uinteger_t >( val ) ) ); |
| } |
| } |
| |
| return( ExpressionConstructor::newInteger( |
| Z3_get_numeral_string(CTX, z3Form)) ); |
| } |
| case Z3_REAL_SORT: |
| { |
| __int64 num; |
| __int64 den; |
| if( Z3_get_numeral_rational_int64(CTX, z3Form, &num, &den) == Z3_L_TRUE ) |
| { |
| return( ExpressionConstructor::newRational( |
| static_cast< avm_integer_t >( num ), |
| static_cast< avm_integer_t >( den ) ) ); |
| } |
| |
| return( ExpressionConstructor::newFloat( |
| Z3_get_numeral_string(CTX, z3Form)) ); |
| } |
| case Z3_UNINTERPRETED_SORT: |
| case Z3_BV_SORT: |
| case Z3_ARRAY_SORT: |
| case Z3_DATATYPE_SORT: |
| default: |
| { |
| return( ExpressionConstructor::newString( |
| Z3_get_numeral_string(CTX, z3Form)) ); |
| |
| break; |
| } |
| } |
| |
| break; |
| } |
| case Z3_APP_AST: |
| { |
| Z3_app app = Z3_to_app(CTX, z3Form); |
| |
| if( Z3_get_app_num_args(CTX, app) == 0 ) |
| { |
| Z3_func_decl func_decl = Z3_get_app_decl(CTX, app); |
| |
| std::string val = Z3_func_decl_to_string(CTX, func_decl); |
| if( val == "(define true bool)" ) |
| { |
| return( ExpressionConstructor::newBoolean( true ) ); |
| } |
| else if( val == "(define false bool)" ) |
| { |
| return( ExpressionConstructor::newBoolean( false ) ); |
| } |
| |
| // z3Form = Z3_model_get_const_interp(CTX, model, func_decl); |
| // |
| // return( to_baseform(model, z3Form) ); |
| |
| } |
| |
| break; |
| } |
| case Z3_QUANTIFIER_AST: |
| { |
| break; |
| } |
| default: |
| { |
| break; |
| } |
| } |
| |
| return( BF::REF_NULL ); |
| } |
| |
| |
| /** |
| * Using file API |
| */ |
| |
| SolverDef::SATISFIABILITY_RING Z3Solver::smt_check_sat(const BF & aCondition) |
| { |
| SolverDef::SATISFIABILITY_RING satisfiability = SolverDef::SATISFIABLE; |
| |
| BFVector paramVector; |
| |
| StringOutStream ossCondition("", "\t", ""); |
| to_smt(ossCondition, aCondition, paramVector); |
| |
| std::string fileLocation = OSS() << mLogFolderLocation |
| << "z3_check_sat_" << SOLVER_SESSION_ID << ".smt"; |
| std::ofstream osFile; |
| osFile.open(fileLocation.c_str(), std::ios_base::out); |
| if ( osFile.good() ) |
| { |
| // osFile << "(echo \"" << aCondition.str() << "\")" << std::endl; |
| |
| InstanceOfData * aParam; |
| |
| std::size_t paramCount = paramVector.size(); |
| for( std::size_t offset = 0 ; offset < paramCount ; offset++ ) |
| { |
| aParam = paramVector[ offset ].to_ptr< InstanceOfData >(); |
| |
| osFile << "(declare-const " << aParam->getFullyQualifiedNameID() |
| << " "; |
| if( aParam->isTypedBoolean() ) |
| { |
| osFile << "Bool"; |
| } |
| else if( aParam->weaklyTypedInteger() || aParam->isTypedEnum() ) |
| { |
| osFile << "Int"; |
| } |
| else if( aParam->weaklyTypedReal() ) |
| { |
| osFile << "Real"; |
| } |
| else |
| { |
| osFile << "Unknown"; |
| } |
| osFile << ")" << std::endl; |
| } |
| |
| osFile << "(assert " << ossCondition.str() << ")" << std::endl; |
| |
| osFile << "(check-sat)" << std::endl; |
| |
| osFile.close(); |
| } |
| else |
| { |
| return( SolverDef::ABORT_SAT ); |
| } |
| |
| |
| return( satisfiability ); |
| } |
| |
| bool Z3Solver::smt_check_model(const BF & aCondition, |
| BFVector & dataVector, BFVector & valuesVector) |
| { |
| BFVector paramVector; |
| |
| StringOutStream ossCondition("", "\t", ""); |
| to_smt(ossCondition, aCondition, paramVector); |
| |
| std::string fileLocation = OSS() << mLogFolderLocation |
| << "z3_check_sat_" << SOLVER_SESSION_ID << ".smt"; |
| std::ofstream osFile; |
| osFile.open(fileLocation.c_str(), std::ios_base::out); |
| if ( osFile.good() ) |
| { |
| // osFile << "(echo \"" << aCondition.str() << "\")" << std::endl; |
| |
| InstanceOfData * aParam; |
| |
| std::size_t paramCount = paramVector.size(); |
| for( std::size_t offset = 0 ; offset < paramCount ; offset++ ) |
| { |
| aParam = paramVector[ offset ].to_ptr< InstanceOfData >(); |
| |
| osFile << "(declare-const " << aParam->getFullyQualifiedNameID() |
| << " "; |
| if( aParam->isTypedBoolean() ) |
| { |
| osFile << "Bool"; |
| } |
| else if( aParam->weaklyTypedInteger() || aParam->isTypedEnum() ) |
| { |
| osFile << "Int"; |
| } |
| else if( aParam->weaklyTypedReal() ) |
| { |
| osFile << "Real"; |
| } |
| else |
| { |
| osFile << "Unknown"; |
| } |
| osFile << ")" << std::endl; |
| } |
| |
| osFile << "(assert " << ossCondition.str() << ")" << std::endl; |
| |
| osFile << "(get-model)" << std::endl; |
| |
| osFile.close(); |
| } |
| else |
| { |
| return( false ); |
| } |
| |
| return( true ); |
| } |
| |
| |
| |
| SolverDef::SATISFIABILITY_RING Z3Solver::from_smt_sat(const BF & aCondition) |
| { |
| SolverDef::SATISFIABILITY_RING satisfiability = SolverDef::SATISFIABLE; |
| |
| |
| return( satisfiability ); |
| } |
| |
| bool Z3Solver::from_smt_model(const BF & aCondition, |
| BFVector & dataVector, BFVector & valuesVector) |
| { |
| return( true ); |
| } |
| |
| |
| |
| void Z3Solver::to_smt(OutStream & os, |
| const BF & exprForm, BFVector & dataVector) const |
| { |
| AVM_OS_ASSERT_FATAL_NULL_SMART_POINTER_EXIT( exprForm ) << "expression !!!" |
| << SEND_EXIT; |
| |
| os << TAB; |
| |
| switch( exprForm.classKind() ) |
| { |
| case FORM_AVMCODE_KIND: |
| { |
| AvmCode * aCode = exprForm.to_ptr< AvmCode >(); |
| |
| os << '('; |
| std::string eoe = ""; |
| |
| switch( aCode->getAvmOpCode() ) |
| { |
| case AVM_OPCODE_AND: |
| { |
| os << "and"; |
| break; |
| } |
| case AVM_OPCODE_OR: |
| { |
| os << "or"; |
| break; |
| } |
| case AVM_OPCODE_NOT: |
| { |
| os << "not"; |
| break; |
| } |
| |
| case AVM_OPCODE_NEQ: |
| { |
| os << "(not"; |
| eoe = ")"; |
| break; |
| } |
| |
| case AVM_OPCODE_IFE: |
| { |
| os << "ite"; |
| break; |
| } |
| |
| case AVM_OPCODE_IF: |
| { |
| os << "if"; |
| break; |
| } |
| |
| default: |
| { |
| os << aCode->getOperator()->strSMT(); |
| break; |
| |
| } |
| } |
| |
| AvmCode::iterator it = aCode->begin(); |
| AvmCode::iterator endIt = aCode->end(); |
| for( ; it != endIt ; ++it ) |
| { |
| os << " "; |
| to_smt(os, *it, dataVector); |
| } |
| |
| os << eoe << ')'; |
| |
| break; |
| } |
| |
| case FORM_INSTANCE_DATA_KIND: |
| { |
| dataVector.add_union( exprForm ); |
| os << exprForm.to_ptr< InstanceOfData >()->getFullyQualifiedNameID(); |
| |
| break; |
| } |
| |
| case FORM_BUILTIN_BOOLEAN_KIND: |
| case FORM_BUILTIN_INTEGER_KIND: |
| case FORM_BUILTIN_RATIONAL_KIND: |
| case FORM_BUILTIN_FLOAT_KIND: |
| { |
| os << exprForm.str(); |
| |
| break; |
| } |
| |
| default: |
| { |
| AVM_OS_FATAL_ERROR_EXIT |
| << "Unexpected BASEFORM KIND as expression << " |
| << exprForm.str() << " >> !!!" |
| << SEND_EXIT; |
| |
| os << exprForm.str(); |
| |
| break; |
| } |
| } |
| |
| os << EOL; |
| } |
| |
| #endif /* _AVM_SOLVER_Z3_CPP_ */ |
| |
| } /* namespace sep */ |
| |
| |
| #endif /* _AVM_SOLVER_Z3_ */ |
| |