Network encodings and heuristics for planning#97

Closed

danbryce wants to merge 30 commits intodreal:masterfrom danbryce:master

+8,396-320

Commits on May 7, 2015

fix(heuristic): avoid backtracking in heuristic unless required

danbryce
authored and
soonhokong
committed
fix(ode_solver): fixed bug in capd formulation that involve double negative --

danbryce
authored and
soonhokong
committed
fix(bmc): added case when there is no relevance analysis

danbryce
authored and
soonhokong
committed
fix(dReach): added parameter for time splitting heuristic

danbryce
authored and
soonhokong
committed
fix(Enode.C): wrapped constants in parens to make negative values safe for CAPD parser

danbryce
authored and
soonhokong
committed
fix(short_sat): Prefer not to branch on irrelevant variables. Added start of new planning heuristic.

danbryce
authored and
soonhokong
committed
fix(THandler): handler was not freezing boolean vars, causing them to be eliminated with prejudice

danbryce
authored and
soonhokong
committed
feat(Debug.C): print Boolean var assignments

danbryce
authored and
soonhokong
committed
feat(heuristics): enhanced plan heuristic

danbryce
authored and
soonhokong
committed
feat(benchmarks): hycirca uav parameter synthesis problem

danbryce
authored and
soonhokong
committed
feat(benchmarks): integer version of modes for battery and heuristics file

danbryce
authored and
soonhokong
committed
feat(heuristics): network heuristics

danbryce
authored and
soonhokong
committed
feat(benchmarks): integer mode encoding of network battery

danbryce
authored and
soonhokong
committed
fix(heuristics): fixed planning heuristics to work with newly refactored heuristic interface

danbryce
authored and
soonhokong
committed
fix(dReach): Reworked substitution stuff

Alexander Heinz
authored and
soonhokong
committed
feat(dReach): extended syntax for network heuristic

danbryce
authored and
soonhokong
committed
feat(heuristics): network heuristics working w/o labels, and added mode mutex constraint to encoding

danbryce
authored and
soonhokong
committed
fix(dReach): invert switch for old/new format

danbryce
authored and
soonhokong
committed
feat(heuristics): heuristic now uses labels for syncing. Also fixed encoding mutex for goal modes.

danbryce
authored and
soonhokong
committed
fix(json): change from json11 dependency and fix rebase issues

danbryce
authored and
soonhokong
committed
feat(dReach): add option to filter encodings

Alexander Heinz
authored and
soonhokong
committed
fix(opensmt) short-sat

danbryce
authored and
soonhokong
committed
fix(opensmt/smtsolvers/CoreSMTSolver.h): define default arg in declaration
soonhokong
committed
fix(heuristics): removed complier warnings

danbryce
authored and
soonhokong
committed
refactor(opensmt/smtsolvers/CoreSMTSolver.C): clean up duplicate code
soonhokong
committed
fix(opensmt/smtsolvers/SimpSMTSolver.C): use nra_found_soln to stop multiple_soln
soonhokong
committed
fix(opensmt/smtsolvers/CoreSMTSolver.h): make CoreSMTSolver::filterUnassigned pure virtual
soonhokong
committed
refactor(opensmt): cleanup whitespace
soonhokong
committed
feat(heuristics): call the appropriate heuristic
danbryce
committed
fix(heuristics): missed some changes to hybrid_heuristic
danbryce
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Network encodings and heuristics for planning#97

Commits on May 7, 2015

fix(heuristic): avoid backtracking in heuristic unless required

fix(ode_solver): fixed bug in capd formulation that involve double negative --

fix(bmc): added case when there is no relevance analysis

fix(dReach): added parameter for time splitting heuristic

fix(Enode.C): wrapped constants in parens to make negative values safe for CAPD parser

fix(short_sat): Prefer not to branch on irrelevant variables. Added start of new planning heuristic.

fix(THandler): handler was not freezing boolean vars, causing them to be eliminated with prejudice

feat(Debug.C): print Boolean var assignments

feat(heuristics): enhanced plan heuristic

feat(benchmarks): hycirca uav parameter synthesis problem

feat(benchmarks): integer version of modes for battery and heuristics file

feat(heuristics): network heuristics

feat(benchmarks): integer mode encoding of network battery

fix(heuristics): fixed planning heuristics to work with newly refactored heuristic interface

fix(dReach): Reworked substitution stuff

feat(dReach): extended syntax for network heuristic

feat(heuristics): network heuristics working w/o labels, and added mode mutex constraint to encoding

fix(dReach): invert switch for old/new format

feat(heuristics): heuristic now uses labels for syncing. Also fixed encoding mutex for goal modes.

fix(json): change from json11 dependency and fix rebase issues

feat(dReach): add option to filter encodings

fix(opensmt) short-sat

fix(opensmt/smtsolvers/CoreSMTSolver.h): define default arg in declaration

fix(heuristics): removed complier warnings

refactor(opensmt/smtsolvers/CoreSMTSolver.C): clean up duplicate code

fix(opensmt/smtsolvers/SimpSMTSolver.C): use nra_found_soln to stop multiple_soln

fix(opensmt/smtsolvers/CoreSMTSolver.h): make CoreSMTSolver::filterUnassigned pure virtual

refactor(opensmt): cleanup whitespace

feat(heuristics): call the appropriate heuristic

fix(heuristics): missed some changes to hybrid_heuristic