2017-06-01 16:16:06 +02:00
# include <anthem/Completion.h>
2017-04-05 18:21:38 +02:00
2017-05-30 03:53:51 +02:00
# include <anthem/AST.h>
2017-06-01 02:37:45 +02:00
# include <anthem/ASTCopy.h>
2017-04-08 16:21:24 +02:00
# include <anthem/ASTUtils.h>
2017-04-05 18:21:38 +02:00
# include <anthem/ASTVisitors.h>
2017-06-01 02:37:45 +02:00
# include <anthem/Exception.h>
2017-06-05 02:50:30 +02:00
# include <anthem/HiddenPredicateElimination.h>
2017-04-10 16:32:12 +02:00
# include <anthem/Utils.h>
2017-04-05 18:21:38 +02:00
namespace anthem
{
////////////////////////////////////////////////////////////////////////////////////////////////////
//
// Completion
//
////////////////////////////////////////////////////////////////////////////////////////////////////
2017-04-10 16:32:12 +02:00
// Builds the conjunction within the completed formula for a given predicate
2017-06-01 02:37:45 +02:00
ast : : Formula buildCompletedFormulaDisjunction ( const ast : : Predicate & predicate , const ast : : VariableDeclarationPointers & parameters , std : : vector < ast : : ScopedFormula > & scopedFormulas )
2017-04-06 17:46:16 +02:00
{
2017-04-10 16:32:12 +02:00
auto disjunction = ast : : Formula : : make < ast : : Or > ( ) ;
2017-04-08 16:21:24 +02:00
2017-06-01 02:37:45 +02:00
assert ( predicate . arguments . size ( ) = = parameters . size ( ) ) ;
2017-04-06 17:46:16 +02:00
2017-06-01 02:37:45 +02:00
// Build the disjunction of all formulas with the predicate as consequent
2017-05-30 03:53:51 +02:00
for ( auto & scopedFormula : scopedFormulas )
2017-04-06 17:46:16 +02:00
{
2017-05-30 03:53:51 +02:00
assert ( scopedFormula . formula . is < ast : : Implies > ( ) ) ;
auto & implies = scopedFormula . formula . get < ast : : Implies > ( ) ;
2017-04-08 18:25:59 +02:00
if ( ! implies . consequent . is < ast : : Predicate > ( ) )
continue ;
2017-04-06 17:46:16 +02:00
auto & otherPredicate = implies . consequent . get < ast : : Predicate > ( ) ;
2017-04-10 16:32:12 +02:00
if ( ! ast : : matches ( predicate , otherPredicate ) )
2017-04-06 17:46:16 +02:00
continue ;
2017-06-01 02:37:45 +02:00
assert ( otherPredicate . arguments . size ( ) = = parameters . size ( ) ) ;
2017-04-08 16:21:24 +02:00
2017-06-01 02:37:45 +02:00
// Each formula with the predicate as its consequent currently has its own copy of the predicate’ s parameters
// These need to be linked to the new, unique set of parameters
for ( size_t i = 0 ; i < parameters . size ( ) ; i + + )
{
assert ( otherPredicate . arguments [ i ] . is < ast : : Variable > ( ) ) ;
const auto & otherVariable = otherPredicate . arguments [ i ] . get < ast : : Variable > ( ) ;
scopedFormula . formula . accept ( ast : : ReplaceVariableInFormulaVisitor ( ) , scopedFormula . formula , otherVariable . declaration , parameters [ i ] . get ( ) ) ;
}
// Remove all the head variables, because they are not free variables after completion
const auto isHeadVariable =
[ ] ( const auto & variableDeclaration )
{
return variableDeclaration - > type = = ast : : VariableDeclaration : : Type : : Head ;
} ;
auto & freeVariables = scopedFormula . freeVariables ;
freeVariables . erase ( std : : remove_if ( freeVariables . begin ( ) , freeVariables . end ( ) , isHeadVariable ) , freeVariables . end ( ) ) ;
if ( freeVariables . empty ( ) )
disjunction . get < ast : : Or > ( ) . arguments . emplace_back ( std : : move ( implies . antecedent ) ) ;
2017-04-08 16:21:24 +02:00
else
{
2017-06-01 02:37:45 +02:00
auto exists = ast : : Formula : : make < ast : : Exists > ( std : : move ( freeVariables ) , std : : move ( implies . antecedent ) ) ;
2017-04-10 16:32:12 +02:00
disjunction . get < ast : : Or > ( ) . arguments . emplace_back ( std : : move ( exists ) ) ;
2017-04-08 16:21:24 +02:00
}
2017-06-01 02:37:45 +02:00
}
2017-04-06 17:46:16 +02:00
2017-04-10 16:32:12 +02:00
return disjunction ;
}
////////////////////////////////////////////////////////////////////////////////////////////////////
// Builds the quantified inner part of the completed formula
ast : : Formula buildCompletedFormulaQuantified ( ast : : Predicate & & predicate , ast : : Formula & & innerFormula )
{
assert ( innerFormula . is < ast : : Or > ( ) ) ;
2017-06-01 02:37:45 +02:00
if ( innerFormula . get < ast : : Or > ( ) . arguments . empty ( ) )
2017-04-10 16:32:12 +02:00
return ast : : Formula : : make < ast : : Not > ( std : : move ( predicate ) ) ;
2017-04-08 20:17:01 +02:00
2017-04-10 16:32:12 +02:00
if ( innerFormula . get < ast : : Or > ( ) . arguments . size ( ) = = 1 )
innerFormula = std : : move ( innerFormula . get < ast : : Or > ( ) . arguments . front ( ) ) ;
2017-04-08 20:17:01 +02:00
2017-04-10 16:32:12 +02:00
if ( innerFormula . is < ast : : Boolean > ( ) )
2017-04-08 20:17:01 +02:00
{
2017-04-10 16:32:12 +02:00
const auto & boolean = innerFormula . get < ast : : Boolean > ( ) ;
2017-04-08 20:17:01 +02:00
if ( boolean . value = = true )
2017-04-10 16:32:12 +02:00
return std : : move ( predicate ) ;
2017-04-08 20:17:01 +02:00
else
2017-04-10 16:32:12 +02:00
return ast : : Formula : : make < ast : : Not > ( std : : move ( predicate ) ) ;
2017-06-01 02:37:45 +02:00
}
2017-04-08 16:21:24 +02:00
2017-04-10 16:32:12 +02:00
return ast : : Formula : : make < ast : : Biconditional > ( std : : move ( predicate ) , std : : move ( innerFormula ) ) ;
}
2017-04-08 14:51:16 +02:00
2017-04-10 16:32:12 +02:00
////////////////////////////////////////////////////////////////////////////////////////////////////
2017-06-05 02:50:30 +02:00
ast : : Formula completePredicate ( const ast : : PredicateSignature & predicateSignature , std : : vector < ast : : ScopedFormula > & scopedFormulas )
2017-04-10 16:32:12 +02:00
{
2017-06-01 02:37:45 +02:00
// Create new set of parameters for the completed definition for the predicate
ast : : VariableDeclarationPointers parameters ;
2017-06-05 02:50:30 +02:00
parameters . reserve ( predicateSignature . arity ) ;
2017-04-10 16:32:12 +02:00
2017-06-01 02:37:45 +02:00
std : : vector < ast : : Term > arguments ;
2017-06-05 02:50:30 +02:00
arguments . reserve ( predicateSignature . arity ) ;
2017-06-01 02:37:45 +02:00
2017-06-05 02:50:30 +02:00
for ( size_t i = 0 ; i < predicateSignature . arity ; i + + )
2017-04-08 14:51:16 +02:00
{
2017-06-01 02:37:45 +02:00
parameters . emplace_back ( std : : make_unique < ast : : VariableDeclaration > ( ast : : VariableDeclaration : : Type : : Head ) ) ;
arguments . emplace_back ( ast : : Term : : make < ast : : Variable > ( parameters . back ( ) . get ( ) ) ) ;
2017-04-08 14:51:16 +02:00
}
2017-06-05 02:50:30 +02:00
ast : : Predicate predicateCopy ( std : : string ( predicateSignature . name ) , std : : move ( arguments ) ) ;
2017-06-01 02:37:45 +02:00
auto completedFormulaDisjunction = buildCompletedFormulaDisjunction ( predicateCopy , parameters , scopedFormulas ) ;
auto completedFormulaQuantified = buildCompletedFormulaQuantified ( std : : move ( predicateCopy ) , std : : move ( completedFormulaDisjunction ) ) ;
if ( parameters . empty ( ) )
return completedFormulaQuantified ;
return ast : : Formula : : make < ast : : ForAll > ( std : : move ( parameters ) , std : : move ( completedFormulaQuantified ) ) ;
2017-04-06 17:46:16 +02:00
}
////////////////////////////////////////////////////////////////////////////////////////////////////
2017-06-01 02:37:45 +02:00
ast : : Formula completeIntegrityConstraint ( ast : : ScopedFormula & scopedFormula )
2017-04-08 18:25:59 +02:00
{
2017-06-01 02:37:45 +02:00
assert ( scopedFormula . formula . is < ast : : Implies > ( ) ) ;
auto & implies = scopedFormula . formula . get < ast : : Implies > ( ) ;
2017-04-08 18:25:59 +02:00
assert ( implies . consequent . is < ast : : Boolean > ( ) ) ;
2017-04-10 16:32:12 +02:00
assert ( implies . consequent . get < ast : : Boolean > ( ) . value = = false ) ;
2017-04-08 18:25:59 +02:00
2017-06-01 02:37:45 +02:00
auto argument = ast : : Formula : : make < ast : : Not > ( std : : move ( implies . antecedent ) ) ;
2017-04-08 18:25:59 +02:00
2017-06-01 02:37:45 +02:00
auto & freeVariables = scopedFormula . freeVariables ;
2017-04-08 18:25:59 +02:00
2017-06-01 02:37:45 +02:00
if ( freeVariables . empty ( ) )
return argument ;
2017-04-08 18:25:59 +02:00
2017-06-01 02:37:45 +02:00
return ast : : Formula : : make < ast : : ForAll > ( std : : move ( freeVariables ) , std : : move ( argument ) ) ;
2017-04-08 18:25:59 +02:00
}
////////////////////////////////////////////////////////////////////////////////////////////////////
2017-06-05 02:50:30 +02:00
std : : vector < ast : : Formula > complete ( std : : vector < ast : : ScopedFormula > & & scopedFormulas , Context & context )
2017-04-05 18:21:38 +02:00
{
2017-06-01 02:37:45 +02:00
// Check whether formulas are in normal form
2017-05-30 03:53:51 +02:00
for ( const auto & scopedFormula : scopedFormulas )
2017-04-05 18:21:38 +02:00
{
2017-05-30 03:53:51 +02:00
if ( ! scopedFormula . formula . is < ast : : Implies > ( ) )
2017-06-01 02:37:45 +02:00
throw CompletionException ( " cannot perform completion, formula not in normal form " ) ;
2017-04-05 18:21:38 +02:00
2017-05-30 03:53:51 +02:00
auto & implies = scopedFormula . formula . get < ast : : Implies > ( ) ;
2017-04-05 18:21:38 +02:00
2017-04-08 18:25:59 +02:00
if ( ! implies . consequent . is < ast : : Predicate > ( ) & & ! implies . consequent . is < ast : : Boolean > ( ) )
2017-06-01 02:37:45 +02:00
throw CompletionException ( " cannot perform completion, only single predicates and Booleans supported as formula consequent currently " ) ;
2017-04-05 18:21:38 +02:00
}
2017-04-06 17:46:16 +02:00
2017-06-05 02:50:30 +02:00
std : : vector < ast : : PredicateSignature > predicateSignatures ;
2017-04-10 16:32:12 +02:00
2017-06-01 02:37:45 +02:00
// Get a list of all predicates
2017-05-30 03:53:51 +02:00
for ( const auto & scopedFormula : scopedFormulas )
2017-06-05 02:50:30 +02:00
ast : : collectPredicateSignatures ( scopedFormula . formula , predicateSignatures ) ;
2017-04-10 16:32:12 +02:00
2017-06-05 02:50:30 +02:00
std : : sort ( predicateSignatures . begin ( ) , predicateSignatures . end ( ) ,
[ ] ( const auto & lhs , const auto & rhs )
2017-04-10 16:32:12 +02:00
{
2017-06-05 02:50:30 +02:00
const auto order = std : : strcmp ( lhs . name . c_str ( ) , rhs . name . c_str ( ) ) ;
2017-04-10 16:32:12 +02:00
if ( order ! = 0 )
2017-06-05 02:50:30 +02:00
return ( order < 0 ) ;
2017-04-10 16:32:12 +02:00
2017-06-05 02:50:30 +02:00
return lhs . arity < rhs . arity ;
2017-04-10 16:32:12 +02:00
} ) ;
2017-06-01 02:37:45 +02:00
std : : vector < ast : : Formula > completedFormulas ;
2017-04-10 16:32:12 +02:00
2018-04-05 23:22:25 +02:00
// Warn about incorrect #external declarations
if ( context . externalPredicateSignatures )
for ( const auto & externalPredicateSignature : * context . externalPredicateSignatures )
{
// TODO: avoid code duplication
const auto matchesPredicateSignature =
[ & ] ( const auto & otherPredicateSignature )
{
return ast : : matches ( externalPredicateSignature , otherPredicateSignature ) ;
} ;
const auto matchingPredicateSignature =
std : : find_if ( predicateSignatures . cbegin ( ) , predicateSignatures . cend ( ) , matchesPredicateSignature ) ;
if ( matchingPredicateSignature = = predicateSignatures . cend ( ) )
context . logger . log ( output : : Priority : : Warning ) < < " #external declaration of “ " < < externalPredicateSignature . name < < " / " < < externalPredicateSignature . arity < < " ” does not match any known predicate " ;
}
2017-04-10 16:32:12 +02:00
// Complete predicates
2017-06-05 02:50:30 +02:00
for ( const auto & predicateSignature : predicateSignatures )
2018-04-05 23:22:25 +02:00
{
// Don’ t complete predicates that are declared #external
if ( context . externalPredicateSignatures )
{
const auto matchesPredicateSignature =
[ & ] ( const auto & otherPredicateSignature )
{
return ast : : matches ( predicateSignature , otherPredicateSignature ) ;
} ;
const auto & externalPredicateSignatures = context . externalPredicateSignatures . value ( ) ;
const auto matchingExternalPredicateSignature =
std : : find_if ( externalPredicateSignatures . cbegin ( ) , externalPredicateSignatures . cend ( ) , matchesPredicateSignature ) ;
if ( matchingExternalPredicateSignature ! = externalPredicateSignatures . cend ( ) )
continue ;
}
2017-06-05 02:50:30 +02:00
completedFormulas . emplace_back ( completePredicate ( predicateSignature , scopedFormulas ) ) ;
2018-04-05 23:22:25 +02:00
}
2017-04-10 16:32:12 +02:00
// Complete integrity constraints
2017-05-30 03:53:51 +02:00
for ( auto & scopedFormula : scopedFormulas )
2017-04-10 16:32:12 +02:00
{
2017-05-30 03:53:51 +02:00
auto & implies = scopedFormula . formula . get < ast : : Implies > ( ) ;
2017-04-10 16:32:12 +02:00
if ( ! implies . consequent . is < ast : : Boolean > ( ) )
continue ;
const auto & boolean = implies . consequent . get < ast : : Boolean > ( ) ;
// Rules of the form “F -> #true” are useless
if ( boolean . value = = true )
continue ;
2017-06-01 02:37:45 +02:00
completedFormulas . emplace_back ( completeIntegrityConstraint ( scopedFormula ) ) ;
2017-04-10 16:32:12 +02:00
}
2017-06-05 02:50:30 +02:00
// Eliminate all predicates that should not be visible in the output
eliminateHiddenPredicates ( predicateSignatures , completedFormulas , context ) ;
2017-06-01 02:37:45 +02:00
return completedFormulas ;
2017-04-05 18:21:38 +02:00
}
////////////////////////////////////////////////////////////////////////////////////////////////////
}